Theorems · Inductive type · Lie groups
OpenAddSubgroup
(G : Type u_1) → [AddGroup G] → [TopologicalSpace G] → Type u_1
The type of open subgroups of a topological additive group.
- Defined in
- Mathlib.Topology.Algebra.OpenSubgroup
- Cited by
- 47 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- AddGroupTopologicalSpace
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
- AddGroupstatement · cited by 4,410
Cited by72
Results whose statement or proof uses this declaration.
- OpenAddSubgroup.toAddSubgroupstatement and proof · cited by 27
- OpenAddSubgroup.isOpenstatement and proof · cited by 7
- OpenNormalAddSubgroup.toOpenAddSubgroupstatement · cited by 6
- OpenAddSubgroup.comapstatement and proof · cited by 5
- NonarchimedeanAddGroup.is_nonarchimedeanstatement · cited by 5
- OpenAddSubgroup.toOpensstatement and proof · cited by 4
- OpenAddSubgroup.isClosedstatement and proof · cited by 3
- OpenAddSubgroup.isOpen'statement and proof · cited by 3
- OpenAddSubgroup.mem_nhds_zerostatement and proof · cited by 2
- OpenAddSubgroup.mem_toAddSubgroupstatement and proof · cited by 2
- OpenAddSubgroup.prodstatement and proof · cited by 2
- OpenAddSubgroup.extstatement and proof · cited by 1