Theorems · Theorem · Lie groups

QuotientGroup.dense_image_mk

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

Defined in

Mathlib.Topology.Algebra.Group.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupSeparatelyContinuousMul