Theorems · Theorem · Lie groups

QuotientAddGroup.dense_image_mk

∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G}
  {s : Set G}, Dense (QuotientAddGroup.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

TopologicalSpaceAddGroupSeparatelyContinuousAdd