Theorems · Theorem · Lie groups

Subgroup.discreteTopology_iff_of_finiteIndex

∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {H : Subgroup G}
  [H.FiniteIndex], DiscreteTopology ↥H ↔ DiscreteTopology G

If G is a topological group and H a finite-index subgroup, then G is topologically discrete iff H is.

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpaceIsTopologicalGroupT2SpaceSubgroup.FiniteIndex