OpenSubgroup

📁 Source: Mathlib/Topology/Algebra/OpenSubgroup.lean

Statistics

Metric	Count
Definitions `addNegClosureNhd`, `mulInvClosureNhd`, `OpenAddSubgroup`, `comap`, `hasCoeAddSubgroup`, `hasCoeOpens`, `instInfOpenAddSubgroup`, `instInhabited`, `instLattice`, `instMax`, `instOrderTop`, `instPartialOrder`, `instPartialOrderOpenAddSubgroup`, `instSemilatticeInfOpenAddSubgroup`, `instSetLike`, `instTop`, `prod`, `toAddSubgroup`, `toOpens`, `OpenNormalAddSubgroup`, `instCoeAddSubgroup`, `instInfOpenNormalAddSubgroup`, `instLatticeOfContinuousAdd`, `instMaxOfContinuousAdd`, `instPartialOrder`, `instPartialOrderOpenNormalAddSubgroup`, `instSemilatticeInfOpenNormalAddSubgroup`, `instSemilatticeSupOpenNormalAddSubgroup`, `instSetLike`, `toOpenAddSubgroup`, `OpenNormalSubgroup`, `instCoeSubgroup`, `instInfOpenNormalSubgroup`, `instLatticeOfContinuousMul`, `instMaxOfContinuousMul`, `instPartialOrder`, `instPartialOrderOpenNormalSubgroup`, `instSemilatticeInfOpenNormalSubgroup`, `instSemilatticeSupOpenNormalSubgroup`, `instSetLike`, `toOpenSubgroup`, `OpenSubgroup`, `comap`, `hasCoeOpens`, `hasCoeSubgroup`, `instInfOpenSubgroup`, `instInhabited`, `instLattice`, `instMax`, `instOrderTop`, `instPartialOrder`, `instPartialOrderOpenSubgroup`, `instSemilatticeInfOpenSubgroup`, `instSetLike`, `instTop`, `prod`, `toOpens`, `toSubgroup`	58
Theorems `addSubgroupOf_isOpen`, `discreteTopology`, `instDiscreteTopologyQuotientOfContinuousAdd`, `instFiniteQuotientOfContinuousAddOfCompactSpace`, `instFiniteQuotientSubtypeMemOpenAddSubgroupOfIsTopologicalAddGroupOfCompactSpace`, `isClosed_of_isOpen`, `isOpen_mono`, `isOpen_of_mem_nhds`, `isOpen_of_openAddSubgroup`, `isOpen_of_zero_mem_interior`, `quotient_finite_of_isOpen`, `quotient_finite_of_isOpen'`, `isOpen_of_isOpen_subideal`, `add`, `isOpen`, `neg`, `nhds`, `exist_add_closure_nhds`, `exist_openAddSubgroup_sub_clopen_nhds_of_zero`, `exists_addNegClosureNhd`, `exist_mul_closure_nhds`, `exist_openSubgroup_sub_clopen_nhds_of_one`, `exists_mulInvClosureNhd`, `inv`, `isOpen`, `mul`, `nhds`, `coe_comap`, `coe_inf`, `coe_prod`, `coe_toAddSubgroup`, `coe_toOpens`, `coe_top`, `comap_comap`, `ext`, `ext_iff`, `instAddSubgroupClass`, `isClopen`, `isClosed`, `isOpen`, `isOpen'`, `mem_comap`, `mem_inf`, `mem_nhds_zero`, `mem_toAddSubgroup`, `mem_toOpens`, `mem_top`, `toAddSubgroup_comap`, `toAddSubgroup_inf`, `toAddSubgroup_injective`, `toAddSubgroup_le`, `toAddSubgroup_prod`, `toAddSubgroup_sup`, `toAddSubgroup_top`, `toOpens_inf`, `toOpens_top`, `ext`, `ext_iff`, `instAddSubgroupClass`, `instNormal`, `isNormal'`, `toAddSubgroup_injective`, `ext`, `ext_iff`, `instNormal`, `instSubgroupClass`, `isNormal'`, `toSubgroup_injective`, `coe_comap`, `coe_inf`, `coe_prod`, `coe_toOpens`, `coe_toSubgroup`, `coe_top`, `comap_comap`, `ext`, `ext_iff`, `instSubgroupClass`, `isClopen`, `isClosed`, `isOpen`, `isOpen'`, `mem_comap`, `mem_inf`, `mem_nhds_one`, `mem_toOpens`, `mem_toSubgroup`, `mem_top`, `toOpens_inf`, `toOpens_top`, `toSubgroup_comap`, `toSubgroup_inf`, `toSubgroup_injective`, `toSubgroup_le`, `toSubgroup_prod`, `toSubgroup_sup`, `toSubgroup_top`, `discreteTopology`, `instDiscreteTopologyQuotientOfContinuousMul`, `instFiniteQuotientOfContinuousMulOfCompactSpace`, `instFiniteQuotientSubtypeMemOpenSubgroupOfIsTopologicalGroupOfCompactSpace`, `isClosed_of_isOpen`, `isOpen_mono`, `isOpen_of_mem_nhds`, `isOpen_of_one_mem_interior`, `isOpen_of_openSubgroup`, `quotient_finite_of_isOpen`, `quotient_finite_of_isOpen'`, `subgroupOf_isOpen`, `isOpen_mono`	110
Total	168

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSubgroupOf_isOpen` 📖	mathematical	`IsOpen` `SetLike.coe` `AddSubgroup` `instSetLike`	`SetLike.instMembership` `instTopologicalSpaceSubtype` `toAddGroup` `addSubgroupOf`	—	`Continuous.isOpen_preimage` `continuous_iff_le_induced`
`discreteTopology` 📖	mathematical	`IsOpen` `SetLike.coe` `AddSubgroup` `instSetLike`	`DiscreteTopology` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instTopologicalSpace`	—	`QuotientAddGroup.discreteTopology`
`instDiscreteTopologyQuotientOfContinuousAdd` 📖	mathematical	—	`DiscreteTopology` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `OpenAddSubgroup.toAddSubgroup` `QuotientAddGroup.instTopologicalSpace`	—	`QuotientAddGroup.discreteTopology` `OpenAddSubgroup.isOpen`
`instFiniteQuotientOfContinuousAddOfCompactSpace` 📖	mathematical	—	`Finite` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `OpenAddSubgroup.toAddSubgroup`	—	`quotient_finite_of_isOpen` `OpenAddSubgroup.isOpen`
`instFiniteQuotientSubtypeMemOpenAddSubgroupOfIsTopologicalAddGroupOfCompactSpace` 📖	mathematical	—	`Finite` `HasQuotient.Quotient` `OpenAddSubgroup` `SetLike.instMembership` `OpenAddSubgroup.instSetLike` `AddSubgroup` `AddSubgroupClass.toAddGroup` `OpenAddSubgroup.instAddSubgroupClass` `QuotientAddGroup.instHasQuotientAddSubgroup` `OpenAddSubgroup.toAddSubgroup` `instTopologicalSpaceSubtype`	—	`OpenAddSubgroup.instAddSubgroupClass` `quotient_finite_of_isOpen'` `OpenAddSubgroup.isOpen`
`isClosed_of_isOpen` 📖	mathematical	`IsOpen` `SetLike.coe` `AddSubgroup` `instSetLike`	`IsClosed`	—	`OpenAddSubgroup.isClosed`
`isOpen_mono` 📖	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsOpen` `SetLike.coe` `instSetLike`	—	—	`isOpen_of_mem_nhds` `Filter.mem_of_superset` `IsOpen.mem_nhds` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass`
`isOpen_of_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `SetLike.coe` `AddSubgroup` `instSetLike`	`IsOpen`	—	`isOpen_iff_mem_nhds` `SetLike.mem_coe` `mem_of_mem_nhds` `Continuous.tendsto'` `Continuous.add` `continuous_id` `continuous_const` `add_neg_cancel_left` `Filter.mem_map'` `add_mem_cancel_right` `add_mem` `neg_mem`
`isOpen_of_openAddSubgroup` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `OpenAddSubgroup.toAddSubgroup`	`IsOpen` `SetLike.coe` `instSetLike`	—	`isOpen_mono` `OpenAddSubgroup.isOpen`
`isOpen_of_zero_mem_interior` 📖	mathematical	`Set` `Set.instMembership` `interior` `SetLike.coe` `AddSubgroup` `instSetLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`IsOpen`	—	`isOpen_of_mem_nhds` `mem_interior_iff_mem_nhds`
`quotient_finite_of_isOpen` 📖	mathematical	`IsOpen` `SetLike.coe` `AddSubgroup` `instSetLike`	`Finite` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup`	—	`QuotientAddGroup.discreteTopology` `finite_of_compact_of_discrete` `QuotientAddGroup.instCompactSpaceQuotientAddSubgroup`
`quotient_finite_of_isOpen'` 📖	mathematical	`IsOpen` `SetLike.coe` `AddSubgroup` `instSetLike` `SetLike.instMembership` `instTopologicalSpaceSubtype` `toAddGroup`	`Finite` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup`	—	`isCompact_iff_compactSpace` `IsClosed.isCompact` `isClosed_of_isOpen` `IsTopologicalAddGroup.toContinuousAdd` `quotient_finite_of_isOpen` `instIsTopologicalAddGroupSubtypeMem`

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_of_isOpen_subideal` 📖	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsOpen` `SetLike.coe` `Submodule.setLike`	—	—	`Submodule.isOpen_mono` `IsTopologicalRing.to_topologicalAddGroup`

IsTopologicalAddGroup

Definitions

Name	Category	Theorems
`addNegClosureNhd` 📖	CompData	1 math math: `exists_addNegClosureNhd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exist_add_closure_nhds` 📖	mathematical	`IsClopen`	`Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Set.instHasSubset` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`IsCompact.induction_on` `IsClosed.isCompact` `IsClopen.isClosed` `Filter.univ_mem` `Set.empty_add` `Set.empty_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.add_subset_add_right` `Filter.inter_mem` `Set.union_add` `Set.union_subset` `Set.add_subset_add_left` `Set.inter_subset_left` `Set.inter_subset_right` `Set.mem_preimage` `add_zero` `isOpen_prod_iff` `Continuous.isOpen_preimage` `continuous_add` `toContinuousAdd` `Set.add_subset_iff` `Set.mk_mem_prod` `IsOpen.mem_nhds`
`exist_openAddSubgroup_sub_clopen_nhds_of_zero` 📖	mathematical	`IsClopen` `Set` `Set.instMembership` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`Set.instHasSubset` `SetLike.coe` `OpenAddSubgroup` `OpenAddSubgroup.instSetLike`	—	`exists_addNegClosureNhd` `Set.mem_iUnion` `add_assoc` `add_nsmul` `Set.add_mem_add` `zero_add` `one_nsmul` `mem_of_mem_nhds` `addNegClosureNhd.nhds` `addNegClosureNhd.neg` `neg_nsmul` `Set.mem_neg` `neg_neg` `isOpen_iUnion` `succ_nsmul` `IsOpen.add_left` `VAddAssocClass.continuousConstVAdd` `VAddAssocClass.left` `toContinuousAdd` `addNegClosureNhd.isOpen` `addNegClosureNhd.add` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.add_subset_add_right` `Set.mem_add` `Set.iUnion_subset`
`exists_addNegClosureNhd` 📖	mathematical	`IsClopen`	`addNegClosureNhd`	—	`exist_add_closure_nhds` `mem_nhds_iff` `Filter.inter_mem_iff` `IsOpen.mem_nhds` `neg_mem_nhds_zero` `Set.inter_neg` `neg_neg` `Set.inter_comm` `IsOpen.inter` `IsOpen.neg` `toContinuousNeg` `Set.add_subset_add_left` `Set.inter_subset_left`

IsTopologicalAddGroup.addNegClosureNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsTopologicalAddGroup.addNegClosureNhd`	`Set` `Set.instHasSubset` `Set.add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`isOpen` 📖	mathematical	`IsTopologicalAddGroup.addNegClosureNhd`	`IsOpen`	—	—
`neg` 📖	mathematical	`IsTopologicalAddGroup.addNegClosureNhd`	`Set` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`nhds` 📖	mathematical	`IsTopologicalAddGroup.addNegClosureNhd`	`Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—

IsTopologicalGroup

Definitions

Name	Category	Theorems
`mulInvClosureNhd` 📖	CompData	1 math math: `exists_mulInvClosureNhd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exist_mul_closure_nhds` 📖	mathematical	`IsClopen`	`Set` `Filter` `Filter.instMembership` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set.instHasSubset` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`IsCompact.induction_on` `IsClosed.isCompact` `IsClopen.isClosed` `Set.empty_mul` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.mul_subset_mul_right` `Filter.inter_mem` `Set.union_mul` `Set.union_subset` `Set.mul_subset_mul_left` `Set.inter_subset_left` `Set.inter_subset_right` `mul_one` `isOpen_prod_iff` `Continuous.isOpen_preimage` `continuous_mul` `toContinuousMul` `Set.mul_subset_iff` `Set.mk_mem_prod` `IsOpen.mem_nhds`
`exist_openSubgroup_sub_clopen_nhds_of_one` 📖	mathematical	`IsClopen` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Set.instHasSubset` `SetLike.coe` `OpenSubgroup` `OpenSubgroup.instSetLike`	—	`exists_mulInvClosureNhd` `Set.mem_iUnion` `add_assoc` `pow_add` `Set.mul_mem_mul` `zero_add` `pow_one` `mem_of_mem_nhds` `mulInvClosureNhd.nhds` `mulInvClosureNhd.inv` `inv_pow` `inv_inv` `isOpen_iUnion` `pow_succ` `IsOpen.mul_left` `IsScalarTower.continuousConstSMul` `IsScalarTower.left` `toContinuousMul` `mulInvClosureNhd.isOpen` `mulInvClosureNhd.mul` `mul_assoc` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.mul_subset_mul_right` `Set.mem_mul` `one_mul` `Set.iUnion_subset`
`exists_mulInvClosureNhd` 📖	mathematical	`IsClopen`	`mulInvClosureNhd`	—	`exist_mul_closure_nhds` `mem_nhds_iff` `IsOpen.mem_nhds` `Set.inter_inv` `inv_inv` `Set.inter_comm` `IsOpen.inter` `IsOpen.inv` `toContinuousInv` `Set.mul_subset_mul_left` `Set.inter_subset_left`

IsTopologicalGroup.mulInvClosureNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv` 📖	mathematical	`IsTopologicalGroup.mulInvClosureNhd`	`Set` `Set.inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`isOpen` 📖	mathematical	`IsTopologicalGroup.mulInvClosureNhd`	`IsOpen`	—	—
`mul` 📖	mathematical	`IsTopologicalGroup.mulInvClosureNhd`	`Set` `Set.instHasSubset` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`nhds` 📖	mathematical	`IsTopologicalGroup.mulInvClosureNhd`	`Set` `Filter` `Filter.instMembership` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—

OpenAddSubgroup

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	4 math math: `coe_comap`, `mem_comap`, `comap_comap`, `toAddSubgroup_comap`
`hasCoeAddSubgroup` 📖	CompOp	—
`hasCoeOpens` 📖	CompOp	—
`instInfOpenAddSubgroup` 📖	CompOp	4 math math: `mem_inf`, `toOpens_inf`, `toAddSubgroup_inf`, `coe_inf`
`instInhabited` 📖	CompOp	—
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	1 math math: `toAddSubgroup_sup`
`instOrderTop` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instPartialOrderOpenAddSubgroup` 📖	CompOp	1 math math: `toAddSubgroup_le`
`instSemilatticeInfOpenAddSubgroup` 📖	CompOp	—
`instSetLike` 📖	CompOp	26 math math: `coe_comap`, `isClopen`, `NonarchimedeanRing.left_mul_subset`, `IsTopologicalAddGroup.exist_openAddSubgroup_sub_clopen_nhds_of_zero`, `mem_inf`, `NonarchimedeanAddGroup.exists_openAddSubgroup_separating`, `mem_comap`, `isOpen`, `mem_nhds_zero`, `coe_toAddSubgroup`, `NonarchimedeanRing.is_nonarchimedean`, `NonarchimedeanRing.mul_subset`, `coe_top`, `isClosed`, `coe_toOpens`, `mem_top`, `NonarchimedeanAddGroup.prod_subset`, `NonarchimedeanAddGroup.is_nonarchimedean`, `mem_toOpens`, `ext_iff`, `mem_toAddSubgroup`, `coe_prod`, `NonarchimedeanAddGroup.prod_self_subset`, `coe_inf`, `AddSubgroup.instFiniteQuotientSubtypeMemOpenAddSubgroupOfIsTopologicalAddGroupOfCompactSpace`, `instAddSubgroupClass`
`instTop` 📖	CompOp	4 math math: `coe_top`, `mem_top`, `toAddSubgroup_top`, `toOpens_top`
`prod` 📖	CompOp	2 math math: `toAddSubgroup_prod`, `coe_prod`
`toAddSubgroup` 📖	CompOp	17 math math: `toAddSubgroup_injective`, `toAddSubgroup_prod`, `OpenNormalAddSubgroup.toAddSubgroup_injective`, `toAddSubgroup_le`, `AddSubgroup.instFiniteQuotientOfContinuousAddOfCompactSpace`, `OpenNormalAddSubgroup.instNormal`, `toAddSubgroup_sup`, `coe_toAddSubgroup`, `AddSubgroup.instDiscreteTopologyQuotientOfContinuousAdd`, `isOpen'`, `toAddSubgroup_inf`, `OpenNormalAddSubgroup.isNormal'`, `toAddSubgroup_top`, `toAddSubgroup_comap`, `mem_toAddSubgroup`, `OpenNormalAddSubgroup.ext_iff`, `AddSubgroup.instFiniteQuotientSubtypeMemOpenAddSubgroupOfIsTopologicalAddGroupOfCompactSpace`
`toOpens` 📖	CompOp	4 math math: `toOpens_inf`, `coe_toOpens`, `mem_toOpens`, `toOpens_top`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_comap` 📖	mathematical	`Continuous` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	`SetLike.coe` `OpenAddSubgroup` `instSetLike` `comap` `Set.preimage`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `OpenAddSubgroup` `instSetLike` `instInfOpenAddSubgroup` `Set` `Set.instInter`	—	—
`coe_prod` 📖	mathematical	—	`SetLike.coe` `OpenAddSubgroup` `Prod.instAddGroup` `instTopologicalSpaceProd` `instSetLike` `prod` `SProd.sprod` `Set` `Set.instSProd`	—	—
`coe_toAddSubgroup` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `toAddSubgroup` `OpenAddSubgroup` `instSetLike`	—	—
`coe_toOpens` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instSetLike` `toOpens` `OpenAddSubgroup` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `OpenAddSubgroup` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`comap_comap` 📖	mathematical	`Continuous` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	`comap` `AddMonoidHom.comp` `Continuous.comp`	—	—
`ext` 📖	—	`OpenAddSubgroup` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`OpenAddSubgroup` `SetLike.instMembership` `instSetLike`	—	`ext`
`instAddSubgroupClass` 📖	mathematical	—	`AddSubgroupClass` `OpenAddSubgroup` `AddGroup.toSubNegMonoid` `instSetLike`	—	`AddSubsemigroup.add_mem'` `AddSubmonoid.zero_mem'` `AddSubgroup.neg_mem'`
`isClopen` 📖	mathematical	—	`IsClopen` `SetLike.coe` `OpenAddSubgroup` `instSetLike`	—	`isClosed` `isOpen`
`isClosed` 📖	mathematical	—	`IsClosed` `SetLike.coe` `OpenAddSubgroup` `instSetLike`	—	`QuotientAddGroup.discreteTopology` `isOpen` `QuotientAddGroup.t1Space_iff` `T2Space.t1Space` `DiscreteTopology.toT2Space`
`isOpen` 📖	mathematical	—	`IsOpen` `SetLike.coe` `OpenAddSubgroup` `instSetLike`	—	`isOpen'`
`isOpen'` 📖	mathematical	—	`IsOpen` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubmonoid.toAddSubsemigroup` `AddSubgroup.toAddSubmonoid` `toAddSubgroup`	—	—
`mem_comap` 📖	mathematical	`Continuous` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	`OpenAddSubgroup` `SetLike.instMembership` `instSetLike` `comap`	—	—
`mem_inf` 📖	mathematical	—	`OpenAddSubgroup` `SetLike.instMembership` `instSetLike` `instInfOpenAddSubgroup`	—	—
`mem_nhds_zero` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SetLike.coe` `OpenAddSubgroup` `instSetLike`	—	`IsOpen.mem_nhds` `isOpen` `AddSubgroup.zero_mem`
`mem_toAddSubgroup` 📖	mathematical	—	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `toAddSubgroup` `OpenAddSubgroup` `instSetLike`	—	—
`mem_toOpens` 📖	mathematical	—	`TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `toOpens` `OpenAddSubgroup` `instSetLike`	—	—
`mem_top` 📖	mathematical	—	`OpenAddSubgroup` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	—
`toAddSubgroup_comap` 📖	mathematical	`Continuous` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	`toAddSubgroup` `comap` `AddSubgroup.comap`	—	—
`toAddSubgroup_inf` 📖	mathematical	—	`toAddSubgroup` `OpenAddSubgroup` `instInfOpenAddSubgroup` `AddSubgroup` `AddSubgroup.instMin`	—	—
`toAddSubgroup_injective` 📖	mathematical	—	`OpenAddSubgroup` `AddSubgroup` `toAddSubgroup`	—	—
`toAddSubgroup_le` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `toAddSubgroup` `OpenAddSubgroup` `instPartialOrderOpenAddSubgroup`	—	—
`toAddSubgroup_prod` 📖	mathematical	—	`toAddSubgroup` `Prod.instAddGroup` `instTopologicalSpaceProd` `prod` `AddSubgroup.prod`	—	—
`toAddSubgroup_sup` 📖	mathematical	—	`toAddSubgroup` `OpenAddSubgroup` `instMax` `AddSubgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `AddSubgroup.instCompleteLattice`	—	—
`toAddSubgroup_top` 📖	mathematical	—	`toAddSubgroup` `Top.top` `OpenAddSubgroup` `instTop` `AddSubgroup` `AddSubgroup.instTop`	—	—
`toOpens_inf` 📖	mathematical	—	`toOpens` `OpenAddSubgroup` `instInfOpenAddSubgroup` `TopologicalSpace.Opens` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	—	—
`toOpens_top` 📖	mathematical	—	`toOpens` `Top.top` `OpenAddSubgroup` `instTop` `TopologicalSpace.Opens` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	—

OpenNormalAddSubgroup

Definitions

Name	Category	Theorems
`instCoeAddSubgroup` 📖	CompOp	—
`instInfOpenNormalAddSubgroup` 📖	CompOp	—
`instLatticeOfContinuousAdd` 📖	CompOp	—
`instMaxOfContinuousAdd` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instPartialOrderOpenNormalAddSubgroup` 📖	CompOp	—
`instSemilatticeInfOpenNormalAddSubgroup` 📖	CompOp	—
`instSemilatticeSupOpenNormalAddSubgroup` 📖	CompOp	—
`instSetLike` 📖	CompOp	3 math math: `instAddSubgroupClass`, `instIsClosedCoePathComponentZero`, `pathComponentZero_carrier`
`toOpenAddSubgroup` 📖	CompOp	4 math math: `toAddSubgroup_injective`, `instNormal`, `isNormal'`, `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubmonoid.toAddSubsemigroup` `AddSubgroup.toAddSubmonoid` `OpenAddSubgroup.toAddSubgroup` `toOpenAddSubgroup`	—	—	—
`ext_iff` 📖	mathematical	—	`AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubmonoid.toAddSubsemigroup` `AddSubgroup.toAddSubmonoid` `OpenAddSubgroup.toAddSubgroup` `toOpenAddSubgroup`	—	`ext`
`instAddSubgroupClass` 📖	mathematical	—	`AddSubgroupClass` `OpenNormalAddSubgroup` `AddGroup.toSubNegMonoid` `instSetLike`	—	`AddSubsemigroup.add_mem'` `AddSubmonoid.zero_mem'` `AddSubgroup.neg_mem'`
`instNormal` 📖	mathematical	—	`AddSubgroup.Normal` `OpenAddSubgroup.toAddSubgroup` `toOpenAddSubgroup`	—	`isNormal'`
`isNormal'` 📖	mathematical	—	`AddSubgroup.Normal` `OpenAddSubgroup.toAddSubgroup` `toOpenAddSubgroup`	—	—
`toAddSubgroup_injective` 📖	mathematical	—	`OpenNormalAddSubgroup` `AddSubgroup` `OpenAddSubgroup.toAddSubgroup` `toOpenAddSubgroup`	—	`ext` `Set.ext`

OpenNormalSubgroup

Definitions

Name	Category	Theorems
`instCoeSubgroup` 📖	CompOp	—
`instInfOpenNormalSubgroup` 📖	CompOp	—
`instLatticeOfContinuousMul` 📖	CompOp	—
`instMaxOfContinuousMul` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instPartialOrderOpenNormalSubgroup` 📖	CompOp	11 math math: `ProfiniteGrp.toLimit_surjective`, `ProfiniteGrp.denseRange_toLimit`, `ProfiniteGrp.cone_pt`, `instFiniteObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor`, `ProfiniteGrp.cone_π_app`, `ProfiniteGrp.toLimit_injective`, `instNonemptyObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor`, `ProfiniteGrp.toLimitFun_continuous`, `ProfiniteGrp.diagram_map`, `ProfiniteGrp.isIso_toLimit`, `ProfiniteGrp.diagram_obj`
`instSemilatticeInfOpenNormalSubgroup` 📖	CompOp	—
`instSemilatticeSupOpenNormalSubgroup` 📖	CompOp	—
`instSetLike` 📖	CompOp	5 math math: `instIsClosedCoePathComponentOne`, `pathComponentOne_carrier`, `IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one`, `instSubgroupClass`, `ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one`
`toOpenSubgroup` 📖	CompOp	4 math math: `instNormal`, `isNormal'`, `toSubgroup_injective`, `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submonoid.toSubsemigroup` `Subgroup.toSubmonoid` `OpenSubgroup.toSubgroup` `toOpenSubgroup`	—	—	—
`ext_iff` 📖	mathematical	—	`Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submonoid.toSubsemigroup` `Subgroup.toSubmonoid` `OpenSubgroup.toSubgroup` `toOpenSubgroup`	—	`ext`
`instNormal` 📖	mathematical	—	`Subgroup.Normal` `OpenSubgroup.toSubgroup` `toOpenSubgroup`	—	`isNormal'`
`instSubgroupClass` 📖	mathematical	—	`SubgroupClass` `OpenNormalSubgroup` `Group.toDivInvMonoid` `instSetLike`	—	`Subsemigroup.mul_mem'` `Submonoid.one_mem'` `Subgroup.inv_mem'`
`isNormal'` 📖	mathematical	—	`Subgroup.Normal` `OpenSubgroup.toSubgroup` `toOpenSubgroup`	—	—
`toSubgroup_injective` 📖	mathematical	—	`OpenNormalSubgroup` `Subgroup` `OpenSubgroup.toSubgroup` `toOpenSubgroup`	—	`ext` `Set.ext`

OpenSubgroup

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	4 math math: `coe_comap`, `mem_comap`, `comap_comap`, `toSubgroup_comap`
`hasCoeOpens` 📖	CompOp	—
`hasCoeSubgroup` 📖	CompOp	—
`instInfOpenSubgroup` 📖	CompOp	4 math math: `coe_inf`, `mem_inf`, `toSubgroup_inf`, `toOpens_inf`
`instInhabited` 📖	CompOp	—
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	1 math math: `toSubgroup_sup`
`instOrderTop` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instPartialOrderOpenSubgroup` 📖	CompOp	1 math math: `toSubgroup_le`
`instSemilatticeInfOpenSubgroup` 📖	CompOp	—
`instSetLike` 📖	CompOp	23 math math: `isOpen`, `coe_comap`, `mem_toOpens`, `mem_top`, `coe_inf`, `coe_prod`, `NonarchimedeanGroup.exists_openSubgroup_separating`, `NonarchimedeanGroup.prod_subset`, `NonarchimedeanGroup.is_nonarchimedean`, `mem_inf`, `mem_nhds_one`, `instSubgroupClass`, `Subgroup.instFiniteQuotientSubtypeMemOpenSubgroupOfIsTopologicalGroupOfCompactSpace`, `ext_iff`, `coe_top`, `coe_toOpens`, `mem_toSubgroup`, `coe_toSubgroup`, `isClosed`, `mem_comap`, `isClopen`, `IsTopologicalGroup.exist_openSubgroup_sub_clopen_nhds_of_one`, `NonarchimedeanGroup.prod_self_subset`
`instTop` 📖	CompOp	4 math math: `toSubgroup_top`, `mem_top`, `coe_top`, `toOpens_top`
`prod` 📖	CompOp	2 math math: `coe_prod`, `toSubgroup_prod`
`toOpens` 📖	CompOp	4 math math: `mem_toOpens`, `coe_toOpens`, `toOpens_inf`, `toOpens_top`
`toSubgroup` 📖	CompOp	19 math math: `OpenNormalSubgroup.instNormal`, `toSubgroup_le`, `toSubgroup_top`, `Subgroup.instDiscreteTopologyQuotientOfContinuousMul`, `OpenNormalSubgroup.isNormal'`, `toSubgroup_inf`, `Subgroup.instFiniteQuotientSubtypeMemOpenSubgroupOfIsTopologicalGroupOfCompactSpace`, `isOpen'`, `CategoryTheory.PreGaloisCategory.has_decomp_quotients`, `toSubgroup_injective`, `OpenNormalSubgroup.toSubgroup_injective`, `OpenNormalSubgroup.ext_iff`, `mem_toSubgroup`, `coe_toSubgroup`, `Subgroup.instFiniteQuotientOfContinuousMulOfCompactSpace`, `CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup`, `toSubgroup_comap`, `toSubgroup_prod`, `toSubgroup_sup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_comap` 📖	mathematical	`Continuous` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`SetLike.coe` `OpenSubgroup` `instSetLike` `comap` `Set.preimage`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `OpenSubgroup` `instSetLike` `instInfOpenSubgroup` `Set` `Set.instInter`	—	—
`coe_prod` 📖	mathematical	—	`SetLike.coe` `OpenSubgroup` `Prod.instGroup` `instTopologicalSpaceProd` `instSetLike` `prod` `SProd.sprod` `Set` `Set.instSProd`	—	—
`coe_toOpens` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instSetLike` `toOpens` `OpenSubgroup` `instSetLike`	—	—
`coe_toSubgroup` 📖	mathematical	—	`SetLike.coe` `Subgroup` `Subgroup.instSetLike` `toSubgroup` `OpenSubgroup` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `OpenSubgroup` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`comap_comap` 📖	mathematical	`Continuous` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`comap` `MonoidHom.comp` `Continuous.comp`	—	—
`ext` 📖	—	`OpenSubgroup` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`OpenSubgroup` `SetLike.instMembership` `instSetLike`	—	`ext`
`instSubgroupClass` 📖	mathematical	—	`SubgroupClass` `OpenSubgroup` `Group.toDivInvMonoid` `instSetLike`	—	`Subsemigroup.mul_mem'` `Submonoid.one_mem'` `Subgroup.inv_mem'`
`isClopen` 📖	mathematical	—	`IsClopen` `SetLike.coe` `OpenSubgroup` `instSetLike`	—	`isClosed` `isOpen`
`isClosed` 📖	mathematical	—	`IsClosed` `SetLike.coe` `OpenSubgroup` `instSetLike`	—	`QuotientGroup.discreteTopology` `isOpen` `QuotientGroup.t1Space_iff` `T2Space.t1Space` `DiscreteTopology.toT2Space`
`isOpen` 📖	mathematical	—	`IsOpen` `SetLike.coe` `OpenSubgroup` `instSetLike`	—	`isOpen'`
`isOpen'` 📖	mathematical	—	`IsOpen` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submonoid.toSubsemigroup` `Subgroup.toSubmonoid` `toSubgroup`	—	—
`mem_comap` 📖	mathematical	`Continuous` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`OpenSubgroup` `SetLike.instMembership` `instSetLike` `comap`	—	—
`mem_inf` 📖	mathematical	—	`OpenSubgroup` `SetLike.instMembership` `instSetLike` `instInfOpenSubgroup`	—	—
`mem_nhds_one` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SetLike.coe` `OpenSubgroup` `instSetLike`	—	`IsOpen.mem_nhds` `isOpen` `Subgroup.one_mem`
`mem_toOpens` 📖	mathematical	—	`TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `toOpens` `OpenSubgroup` `instSetLike`	—	—
`mem_toSubgroup` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `toSubgroup` `OpenSubgroup` `instSetLike`	—	—
`mem_top` 📖	mathematical	—	`OpenSubgroup` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	—
`toOpens_inf` 📖	mathematical	—	`toOpens` `OpenSubgroup` `instInfOpenSubgroup` `TopologicalSpace.Opens` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	—	—
`toOpens_top` 📖	mathematical	—	`toOpens` `Top.top` `OpenSubgroup` `instTop` `TopologicalSpace.Opens` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	—
`toSubgroup_comap` 📖	mathematical	`Continuous` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`toSubgroup` `comap` `Subgroup.comap`	—	—
`toSubgroup_inf` 📖	mathematical	—	`toSubgroup` `OpenSubgroup` `instInfOpenSubgroup` `Subgroup` `Subgroup.instMin`	—	—
`toSubgroup_injective` 📖	mathematical	—	`OpenSubgroup` `Subgroup` `toSubgroup`	—	—
`toSubgroup_le` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `toSubgroup` `OpenSubgroup` `instPartialOrderOpenSubgroup`	—	—
`toSubgroup_prod` 📖	mathematical	—	`toSubgroup` `Prod.instGroup` `instTopologicalSpaceProd` `prod` `Subgroup.prod`	—	—
`toSubgroup_sup` 📖	mathematical	—	`toSubgroup` `OpenSubgroup` `instMax` `Subgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Subgroup.instCompleteLattice`	—	—
`toSubgroup_top` 📖	mathematical	—	`toSubgroup` `Top.top` `OpenSubgroup` `instTop` `Subgroup` `Subgroup.instTop`	—	—

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`discreteTopology` 📖	mathematical	`IsOpen` `SetLike.coe` `Subgroup` `instSetLike`	`DiscreteTopology` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `QuotientGroup.instTopologicalSpace`	—	`QuotientGroup.discreteTopology`
`instDiscreteTopologyQuotientOfContinuousMul` 📖	mathematical	—	`DiscreteTopology` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `OpenSubgroup.toSubgroup` `QuotientGroup.instTopologicalSpace`	—	`QuotientGroup.discreteTopology` `OpenSubgroup.isOpen`
`instFiniteQuotientOfContinuousMulOfCompactSpace` 📖	mathematical	—	`Finite` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `OpenSubgroup.toSubgroup`	—	`quotient_finite_of_isOpen` `OpenSubgroup.isOpen`
`instFiniteQuotientSubtypeMemOpenSubgroupOfIsTopologicalGroupOfCompactSpace` 📖	mathematical	—	`Finite` `HasQuotient.Quotient` `OpenSubgroup` `SetLike.instMembership` `OpenSubgroup.instSetLike` `Subgroup` `SubgroupClass.toGroup` `OpenSubgroup.instSubgroupClass` `QuotientGroup.instHasQuotientSubgroup` `OpenSubgroup.toSubgroup` `instTopologicalSpaceSubtype`	—	`OpenSubgroup.instSubgroupClass` `quotient_finite_of_isOpen'` `OpenSubgroup.isOpen`
`isClosed_of_isOpen` 📖	mathematical	`IsOpen` `SetLike.coe` `Subgroup` `instSetLike`	`IsClosed`	—	`OpenSubgroup.isClosed`
`isOpen_mono` 📖	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsOpen` `SetLike.coe` `instSetLike`	—	—	`isOpen_of_mem_nhds` `Filter.mem_of_superset` `IsOpen.mem_nhds` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `instSubgroupClass`
`isOpen_of_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `SetLike.coe` `Subgroup` `instSetLike`	`IsOpen`	—	`isOpen_iff_mem_nhds` `SetLike.mem_coe` `mem_of_mem_nhds` `Continuous.tendsto'` `Continuous.mul` `continuous_id` `continuous_const` `mul_inv_cancel_left` `mul_mem_cancel_right` `mul_mem` `inv_mem`
`isOpen_of_one_mem_interior` 📖	mathematical	`Set` `Set.instMembership` `interior` `SetLike.coe` `Subgroup` `instSetLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`IsOpen`	—	`isOpen_of_mem_nhds` `mem_interior_iff_mem_nhds`
`isOpen_of_openSubgroup` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `OpenSubgroup.toSubgroup`	`IsOpen` `SetLike.coe` `instSetLike`	—	`isOpen_mono` `OpenSubgroup.isOpen`
`quotient_finite_of_isOpen` 📖	mathematical	`IsOpen` `SetLike.coe` `Subgroup` `instSetLike`	`Finite` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup`	—	`QuotientGroup.discreteTopology` `finite_of_compact_of_discrete` `QuotientGroup.instCompactSpaceQuotientSubgroup`
`quotient_finite_of_isOpen'` 📖	mathematical	`IsOpen` `SetLike.coe` `Subgroup` `instSetLike` `SetLike.instMembership` `instTopologicalSpaceSubtype` `toGroup`	`Finite` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup`	—	`isCompact_iff_compactSpace` `IsClosed.isCompact` `isClosed_of_isOpen` `IsTopologicalGroup.toContinuousMul` `quotient_finite_of_isOpen` `instIsTopologicalGroupSubtypeMem`
`subgroupOf_isOpen` 📖	mathematical	`IsOpen` `SetLike.coe` `Subgroup` `instSetLike`	`SetLike.instMembership` `instTopologicalSpaceSubtype` `toGroup` `subgroupOf`	—	`Continuous.isOpen_preimage` `continuous_iff_le_induced`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_mono` 📖	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsOpen` `SetLike.coe` `setLike`	—	—	`AddSubgroup.isOpen_mono` `IsTopologicalAddGroup.toContinuousAdd`

(root)

Definitions

Name	Category	Theorems
`OpenAddSubgroup` 📖	CompData	33 math math: `OpenAddSubgroup.toAddSubgroup_injective`, `OpenAddSubgroup.coe_comap`, `OpenAddSubgroup.toAddSubgroup_le`, `OpenAddSubgroup.isClopen`, `NonarchimedeanRing.left_mul_subset`, `IsTopologicalAddGroup.exist_openAddSubgroup_sub_clopen_nhds_of_zero`, `OpenAddSubgroup.mem_inf`, `NonarchimedeanAddGroup.exists_openAddSubgroup_separating`, `OpenAddSubgroup.mem_comap`, `OpenAddSubgroup.toOpens_inf`, `OpenAddSubgroup.isOpen`, `OpenAddSubgroup.mem_nhds_zero`, `OpenAddSubgroup.toAddSubgroup_sup`, `OpenAddSubgroup.coe_toAddSubgroup`, `NonarchimedeanRing.is_nonarchimedean`, `NonarchimedeanRing.mul_subset`, `OpenAddSubgroup.coe_top`, `OpenAddSubgroup.isClosed`, `OpenAddSubgroup.coe_toOpens`, `OpenAddSubgroup.mem_top`, `NonarchimedeanAddGroup.prod_subset`, `OpenAddSubgroup.toAddSubgroup_inf`, `NonarchimedeanAddGroup.is_nonarchimedean`, `OpenAddSubgroup.toAddSubgroup_top`, `OpenAddSubgroup.mem_toOpens`, `OpenAddSubgroup.ext_iff`, `OpenAddSubgroup.toOpens_top`, `OpenAddSubgroup.mem_toAddSubgroup`, `OpenAddSubgroup.coe_prod`, `NonarchimedeanAddGroup.prod_self_subset`, `OpenAddSubgroup.coe_inf`, `AddSubgroup.instFiniteQuotientSubtypeMemOpenAddSubgroupOfIsTopologicalAddGroupOfCompactSpace`, `OpenAddSubgroup.instAddSubgroupClass`
`OpenNormalAddSubgroup` 📖	CompData	5 math math: `OpenNormalAddSubgroup.toAddSubgroup_injective`, `OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroup_injective`, `OpenNormalAddSubgroup.instAddSubgroupClass`, `OpenNormalAddSubgroup.instIsClosedCoePathComponentZero`, `OpenNormalAddSubgroup.pathComponentZero_carrier`
`OpenNormalSubgroup` 📖	CompData	18 math math: `OpenNormalSubgroup.instIsClosedCoePathComponentOne`, `OpenNormalSubgroup.pathComponentOne_carrier`, `ProfiniteGrp.toLimit_surjective`, `IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one`, `OpenNormalSubgroup.instSubgroupClass`, `ProfiniteGrp.denseRange_toLimit`, `ProfiniteGrp.cone_pt`, `instFiniteObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor`, `ProfiniteGrp.cone_π_app`, `ProfiniteGrp.toLimit_injective`, `instNonemptyObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor`, `OpenNormalSubgroup.toSubgroup_injective`, `OpenNormalSubgroup.toFiniteIndexNormalSubgroup_injective`, `ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one`, `ProfiniteGrp.toLimitFun_continuous`, `ProfiniteGrp.diagram_map`, `ProfiniteGrp.isIso_toLimit`, `ProfiniteGrp.diagram_obj`
`OpenSubgroup` 📖	CompData	30 math math: `OpenSubgroup.isOpen`, `OpenSubgroup.toSubgroup_le`, `OpenSubgroup.toSubgroup_top`, `OpenSubgroup.coe_comap`, `OpenSubgroup.mem_toOpens`, `OpenSubgroup.mem_top`, `OpenSubgroup.coe_inf`, `OpenSubgroup.coe_prod`, `NonarchimedeanGroup.exists_openSubgroup_separating`, `NonarchimedeanGroup.prod_subset`, `NonarchimedeanGroup.is_nonarchimedean`, `OpenSubgroup.mem_inf`, `OpenSubgroup.mem_nhds_one`, `OpenSubgroup.toSubgroup_inf`, `OpenSubgroup.instSubgroupClass`, `Subgroup.instFiniteQuotientSubtypeMemOpenSubgroupOfIsTopologicalGroupOfCompactSpace`, `OpenSubgroup.ext_iff`, `OpenSubgroup.coe_top`, `OpenSubgroup.coe_toOpens`, `OpenSubgroup.toOpens_inf`, `OpenSubgroup.toSubgroup_injective`, `OpenSubgroup.mem_toSubgroup`, `OpenSubgroup.coe_toSubgroup`, `OpenSubgroup.isClosed`, `OpenSubgroup.mem_comap`, `OpenSubgroup.toOpens_top`, `OpenSubgroup.isClopen`, `IsTopologicalGroup.exist_openSubgroup_sub_clopen_nhds_of_one`, `NonarchimedeanGroup.prod_self_subset`, `OpenSubgroup.toSubgroup_sup`

---

← Back to Index