ClopenNhdofOne

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

Statistics

Metric	Count
Definitions	0
Theorems exist_openNormalSubgroup_sub_clopen_nhds_of_one, closedSubgroup_eq_sInf_open, exist_openNormalSubgroup_sub_open_nhds_of_one	3
Total	3

IsTopologicalGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exist_openNormalSubgroup_sub_clopen_nhds_of_one 📖	mathematical	IsClopen Set Set.instMembership InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Set.instHasSubset SetLike.coe OpenNormalSubgroup OpenNormalSubgroup.instSetLike	—	exist_openSubgroup_sub_clopen_nhds_of_one Subgroup.finiteIndex_of_finite_quotient Subgroup.instFiniteQuotientOfContinuousMulOfCompactSpace toContinuousMul Subgroup.isOpen_of_isClosed_of_finiteIndex Subgroup.finiteIndex_normalCore Subgroup.normalCore_isClosed OpenSubgroup.isClosed Subgroup.normalCore_normal Subgroup.normalCore_le

ProfiniteGrp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedSubgroup_eq_sInf_open 📖	mathematical	—	ClosedSubgroup.toSubgroup InfSet.sInf Subgroup Subgroup.instInfSet setOf IsOpen SetLike.coe Subgroup.instSetLike Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder	—	le_antisymm le_sInf IsClosed.isOpen_compl IsTopologicalGroup.toContinuousMul Homeomorph.isClosedMap ClosedSubgroup.isClosed' Set.mem_compl inv_mem_iff SubgroupClass.toInvMemClass Subgroup.instSubgroupClass inv_eq_iff_mul_eq_one exist_openNormalSubgroup_sub_open_nhds_of_one Subgroup.mem_sup_of_normal_left OpenNormalSubgroup.instNormal eq_mul_inv_iff_mul_eq mem_leftCoset ClosedSubgroup.instSubgroupClass Subgroup.mem_sInf Subgroup.isOpen_mono le_sup_left OpenSubgroup.isOpen le_sup_right
exist_openNormalSubgroup_sub_open_nhds_of_one 📖	mathematical	IsOpen Set Set.instMembership InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Set.instHasSubset SetLike.coe OpenNormalSubgroup OpenNormalSubgroup.instSetLike	—	Filter.HasBasis.mem_iff' nhds_basis_clopen T25Space.t2Space T3Space.t25Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace TotallyDisconnectedSpace.t1Space NormalSpace.of_regularSpace_lindelofSpace IsTopologicalGroup.regularSpace instLindelofSpaceOfSigmaCompactSpace CompactSpace.sigmaCompact mem_nhds_iff subset_refl Set.instReflSubset IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one

---

← Back to Index