Theorems · Theorem · Lie groups

mapClusterPt_atTop_nsmul_tfae

∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (x y : G),
  [MapClusterPt x Filter.atTop fun x => x • y, MapClusterPt x Filter.atTop fun x => x • y,
      x ∈ closure (Set.range fun x => x • y), x ∈ closure (Set.range fun x => x • y)].TFAE

Defined in

Mathlib.Topology.Algebra.Group.SubmonoidClosure

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddGroupTopologicalSpaceCompactSpaceIsTopologicalAddGroup