Documentation Verification Report

ClosedSubgroup

📁 Source: Mathlib/Topology/Algebra/Group/ClosedSubgroup.lean

Statistics

Metric	Count
Definitions `ClosedAddSubgroup`, `instCoeAddSubgroup`, `instInfClosedAddSubgroup`, `instPartialOrder`, `instSemilatticeInfClosedAddSubgroup`, `instSetLike`, `toAddSubgroup`, `ClosedSubgroup`, `instCoeSubgroup`, `instInfClosedSubgroup`, `instPartialOrder`, `instSemilatticeInfClosedSubgroup`, `instSetLike`, `toSubgroup`	14
Theorems `isOpen_of_isClosed_of_finiteIndex`, `ext`, `ext_iff`, `instAddSubgroupClass`, `instCompactSpaceSubtypeMem`, `isClosed'`, `toAddSubgroup_injective`, `ext`, `ext_iff`, `instCompactSpaceSubtypeMem`, `instSubgroupClass`, `isClosed'`, `toSubgroup_injective`, `isOpen_of_isClosed_of_finiteIndex`, `normalCore_isClosed`	15
Total	29

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_of_isClosed_of_finiteIndex` 📖	mathematical	—	`IsOpen` `SetLike.coe` `AddSubgroup` `instSetLike`	—	`QuotientAddGroup.discreteTopology_iff` `Finite.instDiscreteTopology` `QuotientAddGroup.t1Space_iff` `finite_quotient_of_finiteIndex`

ClosedAddSubgroup

Definitions

Name	Category	Theorems
`instCoeAddSubgroup` 📖	CompOp	—
`instInfClosedAddSubgroup` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instSemilatticeInfClosedAddSubgroup` 📖	CompOp	—
`instSetLike` 📖	CompOp	2 math math: `instAddSubgroupClass`, `instCompactSpaceSubtypeMem`
`toAddSubgroup` 📖	CompOp	3 math math: `ext_iff`, `toAddSubgroup_injective`, `isClosed'`

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` `toAddSubgroup`	—	—	—
`ext_iff` 📖	mathematical	—	`AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubmonoid.toAddSubsemigroup` `AddSubgroup.toAddSubmonoid` `toAddSubgroup`	—	`ext`
`instAddSubgroupClass` 📖	mathematical	—	`AddSubgroupClass` `ClosedAddSubgroup` `AddGroup.toSubNegMonoid` `instSetLike`	—	`AddSubsemigroup.add_mem'` `AddSubmonoid.zero_mem'` `AddSubgroup.neg_mem'`
`instCompactSpaceSubtypeMem` 📖	mathematical	—	`CompactSpace` `ClosedAddSubgroup` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype`	—	`isCompact_iff_compactSpace` `IsClosed.isCompact` `isClosed'`
`isClosed'` 📖	mathematical	—	`IsClosed` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubmonoid.toAddSubsemigroup` `AddSubgroup.toAddSubmonoid` `toAddSubgroup`	—	—
`toAddSubgroup_injective` 📖	mathematical	—	`ClosedAddSubgroup` `AddSubgroup` `toAddSubgroup`	—	`ext` `Set.ext`

ClosedSubgroup

Definitions

Name	Category	Theorems
`instCoeSubgroup` 📖	CompOp	—
`instInfClosedSubgroup` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instSemilatticeInfClosedSubgroup` 📖	CompOp	—
`instSetLike` 📖	CompOp	2 math math: `instSubgroupClass`, `instCompactSpaceSubtypeMem`
`toSubgroup` 📖	CompOp	6 math math: `InfiniteGalois.normalAutEquivQuotient_apply`, `isClosed'`, `InfiniteGalois.fixingSubgroup_fixedField`, `ProfiniteGrp.closedSubgroup_eq_sInf_open`, `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` `toSubgroup`	—	—	—
`ext_iff` 📖	mathematical	—	`Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submonoid.toSubsemigroup` `Subgroup.toSubmonoid` `toSubgroup`	—	`ext`
`instCompactSpaceSubtypeMem` 📖	mathematical	—	`CompactSpace` `ClosedSubgroup` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype`	—	`isCompact_iff_compactSpace` `IsClosed.isCompact` `isClosed'`
`instSubgroupClass` 📖	mathematical	—	`SubgroupClass` `ClosedSubgroup` `Group.toDivInvMonoid` `instSetLike`	—	`Subsemigroup.mul_mem'` `Submonoid.one_mem'` `Subgroup.inv_mem'`
`isClosed'` 📖	mathematical	—	`IsClosed` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submonoid.toSubsemigroup` `Subgroup.toSubmonoid` `toSubgroup`	—	—
`toSubgroup_injective` 📖	mathematical	—	`ClosedSubgroup` `Subgroup` `toSubgroup`	—	`ext` `Set.ext`

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_of_isClosed_of_finiteIndex` 📖	mathematical	—	`IsOpen` `SetLike.coe` `Subgroup` `instSetLike`	—	`QuotientGroup.discreteTopology_iff` `Finite.instDiscreteTopology` `QuotientGroup.t1Space_iff` `finite_quotient_of_finiteIndex`
`normalCore_isClosed` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Subgroup` `instSetLike` `normalCore`	—	`normalCore_eq_iInf_conjAct` `coe_iInf` `isClosed_iInter` `Set.ext` `Set.mem_smul_set_iff_inv_smul_mem` `IsClosed.preimage` `IsTopologicalGroup.continuous_conj`

(root)

Definitions

Name	Category	Theorems
`ClosedAddSubgroup` 📖	CompData	3 math math: `ClosedAddSubgroup.toAddSubgroup_injective`, `ClosedAddSubgroup.instAddSubgroupClass`, `ClosedAddSubgroup.instCompactSpaceSubtypeMem`
`ClosedSubgroup` 📖	CompData	3 math math: `ClosedSubgroup.toSubgroup_injective`, `ClosedSubgroup.instSubgroupClass`, `ClosedSubgroup.instCompactSpaceSubtypeMem`

---

← Back to Index