Theorems · Theorem · Lie groups
AddSubgroup.isOpen_of_isClosed_of_finiteIndex
∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] (H : AddSubgroup G)
[H.FiniteIndex], IsClosed ↑H → IsOpen ↑H- Cited by
- 5 results in Mathlib
- Foundations
- Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- SetLike.coestatement and proof · cited by 8,199
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement and proof · cited by 3,232
- IsOpenstatement · cited by 2,400
- IsClosedstatement and proof · cited by 1,639
- SeparatelyContinuousAddstatement and proof · cited by 83
- AddSubgroup.FiniteIndexstatement and proof · cited by 66
- QuotientAddGroup.discreteTopology_iffproof · cited by 2
Cited by5
Results whose statement or proof uses this declaration.
- Ideal.isOpen_of_isMaximalproof · cited by 1
- Ideal.isOpen_pow_of_isMaximalproof · cited by 1
- IsDedekindDomain.isOpen_of_ne_botproof · cited by 1
- AddSubgroup.discreteTopology_iff_of_finiteIndexproof · cited by 1