Documentation Verification Report

GroupTopology

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

Statistics

Metric	Count
Definitions `AddGroupTopology`, `coinduced`, `instBot`, `instBoundedOrder`, `instCompleteLattice`, `instCompleteSemilatticeInf`, `instInfSet`, `instInhabited`, `instMin`, `instPartialOrder`, `instSemilatticeInf`, `instTop`, `toTopologicalSpace`, `GroupTopology`, `coinduced`, `instBot`, `instBoundedOrder`, `instCompleteLattice`, `instCompleteSemilatticeInf`, `instInfSet`, `instInhabited`, `instMin`, `instPartialOrder`, `instSemilatticeInf`, `instTop`, `toTopologicalSpace`	26
Theorems `coinduced_continuous`, `continuous_add'`, `continuous_neg'`, `ext'`, `ext'_iff`, `toIsTopologicalAddGroup`, `toTopologicalSpace_bot`, `toTopologicalSpace_iInf`, `toTopologicalSpace_inf`, `toTopologicalSpace_injective`, `toTopologicalSpace_le`, `toTopologicalSpace_sInf`, `toTopologicalSpace_top`, `coinduced_continuous`, `continuous_inv'`, `continuous_mul'`, `ext'`, `ext'_iff`, `toIsTopologicalGroup`, `toTopologicalSpace_bot`, `toTopologicalSpace_iInf`, `toTopologicalSpace_inf`, `toTopologicalSpace_injective`, `toTopologicalSpace_le`, `toTopologicalSpace_sInf`, `toTopologicalSpace_top`	26
Total	52

AddGroupTopology

Definitions

Name	Category	Theorems
`coinduced` 📖	CompOp	1 math math: `coinduced_continuous`
`instBot` 📖	CompOp	1 math math: `toTopologicalSpace_bot`
`instBoundedOrder` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	—
`instCompleteSemilatticeInf` 📖	CompOp	—
`instInfSet` 📖	CompOp	2 math math: `toTopologicalSpace_sInf`, `toTopologicalSpace_iInf`
`instInhabited` 📖	CompOp	—
`instMin` 📖	CompOp	1 math math: `toTopologicalSpace_inf`
`instPartialOrder` 📖	CompOp	1 math math: `toTopologicalSpace_le`
`instSemilatticeInf` 📖	CompOp	—
`instTop` 📖	CompOp	1 math math: `toTopologicalSpace_top`
`toTopologicalSpace` 📖	CompOp	12 math math: `toTopologicalSpace_inf`, `toTopologicalSpace_injective`, `toTopologicalSpace_sInf`, `toTopologicalSpace_top`, `continuous_add'`, `toTopologicalSpace_le`, `toIsTopologicalAddGroup`, `coinduced_continuous`, `toTopologicalSpace_iInf`, `ext'_iff`, `continuous_neg'`, `toTopologicalSpace_bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coinduced_continuous` 📖	mathematical	—	`Continuous` `toTopologicalSpace` `coinduced`	—	`continuous_sInf_rng` `continuous_iff_coinduced_le`
`continuous_add'` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `toTopologicalSpace` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`continuous_add` `IsTopologicalAddGroup.toContinuousAdd` `toIsTopologicalAddGroup`
`continuous_neg'` 📖	mathematical	—	`Continuous` `toTopologicalSpace` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ContinuousNeg.continuous_neg` `IsTopologicalAddGroup.toContinuousNeg` `toIsTopologicalAddGroup`
`ext'` 📖	—	`TopologicalSpace.IsOpen` `toTopologicalSpace`	—	—	`toTopologicalSpace_injective` `TopologicalSpace.ext`
`ext'_iff` 📖	mathematical	—	`TopologicalSpace.IsOpen` `toTopologicalSpace`	—	`ext'`
`toIsTopologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `toTopologicalSpace`	—	—
`toTopologicalSpace_bot` 📖	mathematical	—	`toTopologicalSpace` `Bot.bot` `AddGroupTopology` `instBot` `TopologicalSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—
`toTopologicalSpace_iInf` 📖	mathematical	—	`toTopologicalSpace` `iInf` `AddGroupTopology` `instInfSet` `TopologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice`	—	`Set.range_comp`
`toTopologicalSpace_inf` 📖	mathematical	—	`toTopologicalSpace` `AddGroupTopology` `instMin` `TopologicalSpace` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice`	—	—
`toTopologicalSpace_injective` 📖	mathematical	—	`AddGroupTopology` `TopologicalSpace` `toTopologicalSpace`	—	—
`toTopologicalSpace_le` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `toTopologicalSpace` `AddGroupTopology` `instPartialOrder`	—	—
`toTopologicalSpace_sInf` 📖	mathematical	—	`toTopologicalSpace` `InfSet.sInf` `AddGroupTopology` `instInfSet` `TopologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `Set.image`	—	—
`toTopologicalSpace_top` 📖	mathematical	—	`toTopologicalSpace` `Top.top` `AddGroupTopology` `instTop` `TopologicalSpace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	—

GroupTopology

Definitions

Name	Category	Theorems
`coinduced` 📖	CompOp	1 math math: `coinduced_continuous`
`instBot` 📖	CompOp	1 math math: `toTopologicalSpace_bot`
`instBoundedOrder` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	—
`instCompleteSemilatticeInf` 📖	CompOp	—
`instInfSet` 📖	CompOp	2 math math: `toTopologicalSpace_iInf`, `toTopologicalSpace_sInf`
`instInhabited` 📖	CompOp	—
`instMin` 📖	CompOp	1 math math: `toTopologicalSpace_inf`
`instPartialOrder` 📖	CompOp	1 math math: `toTopologicalSpace_le`
`instSemilatticeInf` 📖	CompOp	—
`instTop` 📖	CompOp	1 math math: `toTopologicalSpace_top`
`toTopologicalSpace` 📖	CompOp	12 math math: `toTopologicalSpace_iInf`, `toTopologicalSpace_inf`, `continuous_mul'`, `ext'_iff`, `toTopologicalSpace_sInf`, `toTopologicalSpace_bot`, `toIsTopologicalGroup`, `toTopologicalSpace_le`, `continuous_inv'`, `toTopologicalSpace_top`, `coinduced_continuous`, `toTopologicalSpace_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coinduced_continuous` 📖	mathematical	—	`Continuous` `toTopologicalSpace` `coinduced`	—	`continuous_sInf_rng` `continuous_iff_coinduced_le`
`continuous_inv'` 📖	mathematical	—	`Continuous` `toTopologicalSpace` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`ContinuousInv.continuous_inv` `IsTopologicalGroup.toContinuousInv` `toIsTopologicalGroup`
`continuous_mul'` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `toTopologicalSpace` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`continuous_mul` `IsTopologicalGroup.toContinuousMul` `toIsTopologicalGroup`
`ext'` 📖	—	`TopologicalSpace.IsOpen` `toTopologicalSpace`	—	—	`toTopologicalSpace_injective` `TopologicalSpace.ext`
`ext'_iff` 📖	mathematical	—	`TopologicalSpace.IsOpen` `toTopologicalSpace`	—	`ext'`
`toIsTopologicalGroup` 📖	mathematical	—	`IsTopologicalGroup` `toTopologicalSpace`	—	—
`toTopologicalSpace_bot` 📖	mathematical	—	`toTopologicalSpace` `Bot.bot` `GroupTopology` `instBot` `TopologicalSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—
`toTopologicalSpace_iInf` 📖	mathematical	—	`toTopologicalSpace` `iInf` `GroupTopology` `instInfSet` `TopologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice`	—	`Set.range_comp`
`toTopologicalSpace_inf` 📖	mathematical	—	`toTopologicalSpace` `GroupTopology` `instMin` `TopologicalSpace` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice`	—	—
`toTopologicalSpace_injective` 📖	mathematical	—	`GroupTopology` `TopologicalSpace` `toTopologicalSpace`	—	—
`toTopologicalSpace_le` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `toTopologicalSpace` `GroupTopology` `instPartialOrder`	—	—
`toTopologicalSpace_sInf` 📖	mathematical	—	`toTopologicalSpace` `InfSet.sInf` `GroupTopology` `instInfSet` `TopologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `Set.image`	—	—
`toTopologicalSpace_top` 📖	mathematical	—	`toTopologicalSpace` `Top.top` `GroupTopology` `instTop` `TopologicalSpace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	—

(root)

Definitions

Name	Category	Theorems
`AddGroupTopology` 📖	CompData	7 math math: `AddGroupTopology.toTopologicalSpace_inf`, `AddGroupTopology.toTopologicalSpace_injective`, `AddGroupTopology.toTopologicalSpace_sInf`, `AddGroupTopology.toTopologicalSpace_top`, `AddGroupTopology.toTopologicalSpace_le`, `AddGroupTopology.toTopologicalSpace_iInf`, `AddGroupTopology.toTopologicalSpace_bot`
`GroupTopology` 📖	CompData	7 math math: `GroupTopology.toTopologicalSpace_iInf`, `GroupTopology.toTopologicalSpace_inf`, `GroupTopology.toTopologicalSpace_sInf`, `GroupTopology.toTopologicalSpace_bot`, `GroupTopology.toTopologicalSpace_le`, `GroupTopology.toTopologicalSpace_top`, `GroupTopology.toTopologicalSpace_injective`

---

← Back to Index