Theorems · Theorem · Lie groups

QuotientGroup.dense_preimage_mk

∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {N : Subgroup G}
  {s : Set (G ⧸ N)}, Dense (QuotientGroup.mk ⁻¹' s) ↔ Dense s

Defined in

Mathlib.Topology.Algebra.Group.Quotient

Cited by

1 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceGroupSeparatelyContinuousMul