DiscreteSubgroup

📁 Source: Mathlib/Topology/Algebra/IsUniformGroup/DiscreteSubgroup.lean

Statistics

Metric	Count
Definitions addSubgroupOfContinuousAddEquivOfLe, subgroupOfContinuousMulEquivOfLe	2
Theorems discreteTopology_iff, addSubgroupOfContinuousAddEquivOfLe_apply, addSubgroupOfContinuousAddEquivOfLe_symm_apply, addSubgroupOfContinuousAddEquivOfLe_toAddEquiv, discreteTopology_iff_of_finiteIndex, discreteTopology_iff_of_isFiniteRelIndex, discreteTopology_iff, discreteTopology_iff_of_finiteIndex, discreteTopology_iff_of_isFiniteRelIndex, subgroupOfContinuousMulEquivOfLe_apply, subgroupOfContinuousMulEquivOfLe_symm_apply, subgroupOfContinuousMulEquivOfLe_toMulEquiv	12
Total	14

AddSubgroup

Definitions

Name	Category	Theorems
addSubgroupOfContinuousAddEquivOfLe 📖	CompOp	3 math math: addSubgroupOfContinuousAddEquivOfLe_apply, addSubgroupOfContinuousAddEquivOfLe_symm_apply, addSubgroupOfContinuousAddEquivOfLe_toAddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addSubgroupOfContinuousAddEquivOfLe_apply 📖	mathematical	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe ContinuousAddEquiv SetLike.instMembership instSetLike toAddGroup addSubgroupOf instTopologicalSpaceSubtype add EquivLike.toFunLike ContinuousAddEquiv.instEquivLike addSubgroupOfContinuousAddEquivOfLe AddEquiv AddEquiv.instEquivLike addSubgroupOfEquivOfLe	—	—
addSubgroupOfContinuousAddEquivOfLe_symm_apply 📖	mathematical	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe ContinuousAddEquiv SetLike.instMembership instSetLike instTopologicalSpaceSubtype toAddGroup addSubgroupOf add EquivLike.toFunLike ContinuousAddEquiv.instEquivLike ContinuousAddEquiv.symm addSubgroupOfContinuousAddEquivOfLe	—	—
addSubgroupOfContinuousAddEquivOfLe_toAddEquiv 📖	mathematical	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	AddEquivClass.toAddEquiv ContinuousAddEquiv SetLike.instMembership instSetLike toAddGroup addSubgroupOf instTopologicalSpaceSubtype add ContinuousAddEquiv.instEquivLike ContinuousAddEquiv.instAddEquivClass addSubgroupOfContinuousAddEquivOfLe addSubgroupOfEquivOfLe	—	ContinuousAddEquiv.instAddEquivClass
discreteTopology_iff_of_finiteIndex 📖	mathematical	—	DiscreteTopology AddSubgroup SetLike.instMembership instSetLike instTopologicalSpaceSubtype	—	isOpen_of_isClosed_of_finiteIndex IsTopologicalAddGroup.toContinuousAdd isClosed_of_discrete discreteTopology_iff_isOpen_singleton_zero isOpen_singleton_iff_nhds_eq_pure coe_zero Topology.IsOpenEmbedding.map_nhds_eq IsOpen.isOpenEmbedding_subtypeVal nhds_discrete Filter.map_pure instDiscreteTopologySubtype
discreteTopology_iff_of_isFiniteRelIndex 📖	mathematical	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	DiscreteTopology SetLike.instMembership instSetLike instTopologicalSpaceSubtype	—	Homeomorph.discreteTopology_iff discreteTopology_iff_of_finiteIndex instIsTopologicalAddGroupSubtypeMem instT2SpaceSubtype IsFiniteRelIndex.to_finiteIndex_addSubgroupOf

AddSubgroup.Commensurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discreteTopology_iff 📖	mathematical	AddSubgroup.Commensurable	DiscreteTopology AddSubgroup SetLike.instMembership AddSubgroup.instSetLike instTopologicalSpaceSubtype	—	AddSubgroup.discreteTopology_iff_of_isFiniteRelIndex inf_le_left AddSubgroup.inf_relIndex_left inf_le_right AddSubgroup.inf_relIndex_right

Subgroup

Definitions

Name	Category	Theorems
subgroupOfContinuousMulEquivOfLe 📖	CompOp	3 math math: subgroupOfContinuousMulEquivOfLe_toMulEquiv, subgroupOfContinuousMulEquivOfLe_apply, subgroupOfContinuousMulEquivOfLe_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discreteTopology_iff_of_finiteIndex 📖	mathematical	—	DiscreteTopology Subgroup SetLike.instMembership instSetLike instTopologicalSpaceSubtype	—	isOpen_of_isClosed_of_finiteIndex IsTopologicalGroup.toContinuousMul isClosed_of_discrete discreteTopology_iff_isOpen_singleton_one isOpen_singleton_iff_nhds_eq_pure coe_one Topology.IsOpenEmbedding.map_nhds_eq IsOpen.isOpenEmbedding_subtypeVal nhds_discrete Filter.map_pure instDiscreteTopologySubtype
discreteTopology_iff_of_isFiniteRelIndex 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	DiscreteTopology SetLike.instMembership instSetLike instTopologicalSpaceSubtype	—	Homeomorph.discreteTopology_iff discreteTopology_iff_of_finiteIndex instIsTopologicalGroupSubtypeMem instT2SpaceSubtype IsFiniteRelIndex.to_finiteIndex_subgroupOf
subgroupOfContinuousMulEquivOfLe_apply 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe ContinuousMulEquiv SetLike.instMembership instSetLike toGroup subgroupOf instTopologicalSpaceSubtype mul EquivLike.toFunLike ContinuousMulEquiv.instEquivLike subgroupOfContinuousMulEquivOfLe MulEquiv MulEquiv.instEquivLike subgroupOfEquivOfLe	—	—
subgroupOfContinuousMulEquivOfLe_symm_apply 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe ContinuousMulEquiv SetLike.instMembership instSetLike instTopologicalSpaceSubtype toGroup subgroupOf mul EquivLike.toFunLike ContinuousMulEquiv.instEquivLike ContinuousMulEquiv.symm subgroupOfContinuousMulEquivOfLe	—	—
subgroupOfContinuousMulEquivOfLe_toMulEquiv 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	MulEquivClass.toMulEquiv ContinuousMulEquiv SetLike.instMembership instSetLike toGroup subgroupOf instTopologicalSpaceSubtype mul ContinuousMulEquiv.instEquivLike ContinuousMulEquiv.instMulEquivClass subgroupOfContinuousMulEquivOfLe subgroupOfEquivOfLe	—	ContinuousMulEquiv.instMulEquivClass

Subgroup.Commensurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discreteTopology_iff 📖	mathematical	Subgroup.Commensurable	DiscreteTopology Subgroup SetLike.instMembership Subgroup.instSetLike instTopologicalSpaceSubtype	—	Subgroup.discreteTopology_iff_of_isFiniteRelIndex inf_le_left Subgroup.inf_relIndex_left inf_le_right Subgroup.inf_relIndex_right

---

← Back to Index