Documentation Verification Report

NonUnitalAlgebra

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

Statistics

Metric	Count
Definitions `elemental`, `instNonUnitalCommRingSubtypeMemNonUnitalSubalgebraOfT2Space`, `instNonUnitalCommSemiringSubtypeMemNonUnitalSubalgebraOfT2Space`, `nonUnitalCommRingTopologicalClosure`, `nonUnitalCommSemiringTopologicalClosure`, `topologicalClosure`	6
Theorems `instCompleteSpaceSubtypeMemNonUnitalSubalgebra`, `isClosed`, `isClosedEmbedding_coe`, `le_centralizer_centralizer`, `le_iff_mem`, `le_of_mem`, `self_mem`, `instIsTopologicalRing`, `instIsTopologicalSemiring`, `isClosed_topologicalClosure`, `le_topologicalClosure`, `map_topologicalClosure_le`, `topologicalClosure_adjoin_le_centralizer_centralizer`, `topologicalClosure_map`, `topologicalClosure_map_le`, `topologicalClosure_minimal`	16
Total	22

NonUnitalAlgebra

Definitions

Name	Category	Theorems
`elemental` 📖	CompOp	7 math math: `elemental.isClosedEmbedding_coe`, `elemental.isClosed`, `elemental.le_of_mem`, `elemental.instCompleteSpaceSubtypeMemNonUnitalSubalgebra`, `elemental.le_centralizer_centralizer`, `elemental.le_iff_mem`, `elemental.self_mem`

NonUnitalAlgebra.elemental

Definitions

Name	Category	Theorems
`instNonUnitalCommRingSubtypeMemNonUnitalSubalgebraOfT2Space` 📖	CompOp	—
`instNonUnitalCommSemiringSubtypeMemNonUnitalSubalgebraOfT2Space` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompleteSpaceSubtypeMemNonUnitalSubalgebra` 📖	mathematical	—	`CompleteSpace` `NonUnitalSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `NonUnitalSubalgebra.instSetLike` `NonUnitalAlgebra.elemental` `UniformSpace.toTopologicalSpace` `instUniformSpaceSubtype`	—	`IsClosed.completeSpace_coe` `isClosed_closure`
`isClosed` 📖	mathematical	—	`IsClosed` `SetLike.coe` `NonUnitalSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalSubalgebra.instSetLike` `NonUnitalAlgebra.elemental`	—	`NonUnitalSubalgebra.isClosed_topologicalClosure`
`isClosedEmbedding_coe` 📖	mathematical	—	`Topology.IsClosedEmbedding` `NonUnitalSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `NonUnitalSubalgebra.instSetLike` `NonUnitalAlgebra.elemental` `instTopologicalSpaceSubtype`	—	`Subtype.coe_injective` `Subtype.range_coe_subtype` `isClosed`
`le_centralizer_centralizer` 📖	mathematical	—	`NonUnitalSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalSubalgebra.instPartialOrder` `NonUnitalAlgebra.elemental` `NonUnitalSubalgebra.centralizer` `SetLike.coe` `NonUnitalSubalgebra.instSetLike` `Set` `Set.instSingletonSet`	—	`NonUnitalSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer`
`le_iff_mem` 📖	mathematical	—	`NonUnitalSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalSubalgebra.instPartialOrder` `NonUnitalAlgebra.elemental` `SetLike.instMembership` `NonUnitalSubalgebra.instSetLike`	—	`self_mem` `le_of_mem`
`le_of_mem` 📖	mathematical	`NonUnitalSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `NonUnitalSubalgebra.instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalSubalgebra.instPartialOrder` `NonUnitalAlgebra.elemental`	—	`NonUnitalSubalgebra.topologicalClosure_minimal` `NonUnitalAlgebra.adjoin_le`
`self_mem` 📖	mathematical	—	`NonUnitalSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `NonUnitalSubalgebra.instSetLike` `NonUnitalAlgebra.elemental`	—	`NonUnitalSubalgebra.le_topologicalClosure` `NonUnitalAlgebra.self_mem_adjoin_singleton`

NonUnitalSubalgebra

Definitions

Name	Category	Theorems
`nonUnitalCommRingTopologicalClosure` 📖	CompOp	—
`nonUnitalCommSemiringTopologicalClosure` 📖	CompOp	—
`topologicalClosure` 📖	CompOp	7 math math: `topologicalClosure_minimal`, `topologicalClosure_map_le`, `topologicalClosure_map`, `le_topologicalClosure`, `topologicalClosure_adjoin_le_centralizer_centralizer`, `isClosed_topologicalClosure`, `map_topologicalClosure_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `NonUnitalSubalgebra` `CommRing.toCommSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `toNonUnitalNonAssocRing`	—	`NonUnitalSubring.instIsTopologicalRing`
`instIsTopologicalSemiring` 📖	mathematical	—	`IsTopologicalSemiring` `NonUnitalSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `toNonUnitalNonAssocSemiring`	—	`NonUnitalSubsemiring.instIsTopologicalSemiring`
`isClosed_topologicalClosure` 📖	mathematical	—	`IsClosed` `SetLike.coe` `NonUnitalSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `instSetLike` `topologicalClosure`	—	`isClosed_closure`
`le_topologicalClosure` 📖	mathematical	—	`NonUnitalSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`subset_closure`
`map_topologicalClosure_le` 📖	mathematical	`Continuous` `DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalAlgHom.instFunLike_1`	`NonUnitalSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass` `topologicalClosure`	—	`image_closure_subset_closure_image` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass`
`topologicalClosure_adjoin_le_centralizer_centralizer` 📖	mathematical	—	`NonUnitalSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure` `NonUnitalAlgebra.adjoin` `centralizer` `SetLike.coe` `instSetLike`	—	`topologicalClosure_minimal` `NonUnitalAlgebra.adjoin_le_centralizer_centralizer` `Set.isClosed_centralizer` `IsTopologicalSemiring.toContinuousMul`
`topologicalClosure_map` 📖	mathematical	`IsClosedMap` `DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalAlgHom.instFunLike_1` `Continuous`	`topologicalClosure` `map` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass`	—	`SetLike.coe_injective` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass` `IsClosedMap.closure_image_eq_of_continuous`
`topologicalClosure_map_le` 📖	mathematical	`IsClosedMap` `DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalAlgHom.instFunLike_1`	`NonUnitalSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure` `map` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass`	—	`IsClosedMap.closure_image_subset`
`topologicalClosure_minimal` 📖	mathematical	`NonUnitalSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`topologicalClosure`	—	`closure_minimal`

---

← Back to Index