Theorems · Theorem · Lie groups
Subgroup.discreteTopology_iff_of_isFiniteRelIndex
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {H K : Subgroup G},
H ≤ K → ∀ [H.IsFiniteRelIndex K], DiscreteTopology ↥H ↔ DiscreteTopology ↥K- Cited by
- 1 results in Mathlib
- Foundations
- Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Groupstatement and proof · cited by 6,238
- Subgroupstatement and proof · cited by 3,593
- T2Spacestatement and proof · cited by 1,351
- IsTopologicalGroupstatement and proof · cited by 469
- DiscreteTopologystatement and proof · cited by 373
- Subgroup.subgroupOfproof · cited by 122
- Subgroup.FiniteIndexproof · cited by 113
- Subgroup.IsFiniteRelIndexstatement and proof · cited by 26
- ContinuousMulEquiv.toHomeomorphproof · cited by 8
- Homeomorph.discreteTopology_iffproof · cited by 7
- Subgroup.subgroupOfContinuousMulEquivOfLeproof · cited by 4
Cited by1
Results whose statement or proof uses this declaration.
- Subgroup.Commensurable.discreteTopology_iffproof · cited by 0