Theorems · Inductive type · Lie groups
OpenNormalSubgroup
(G : Type u) → [Group G] → [TopologicalSpace G] → Type u
The type of open normal subgroups of a topological group.
- Defined in
- Mathlib.Topology.Algebra.OpenSubgroup
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- GroupTopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- Groupstatement · cited by 6,238
Cited by49
Results whose statement or proof uses this declaration.
- OpenNormalSubgroup.toOpenSubgroupstatement and proof · cited by 11
- ProfiniteGrp.diagramstatement · cited by 10
- ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_onestatement and proof · cited by 5
- ProfiniteGrp.isoLimittoFiniteQuotientFunctorstatement · cited by 3
- ProfiniteGrp.toFiniteQuotientFunctorstatement and proof · cited by 3
- ProfiniteGrp.toLimitstatement · cited by 3
- ProfiniteGrp.ProfiniteCompletion.liftproof · cited by 3
- ProfiniteGrp.conestatement · cited by 2
- OpenNormalSubgroup.extstatement and proof · cited by 2
- OpenNormalSubgroup.toFiniteIndexNormalSubgroupstatement and proof · cited by 2
- ProfiniteGrp.ProfiniteCompletion.preimagestatement and proof · cited by 2
- Ideal.Quotient.stabilizerHomSurjectiveAuxFunctorstatement and proof · cited by 1