Documentation Verification Report

NonUnitalStarAlgebra

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

Statistics

Metric	Count
Definitions `elemental`, `instNonUnitalCommRingSubtypeMemNonUnitalStarSubalgebraOfT2SpaceOfIsStarNormal`, `instNonUnitalCommSemiringSubtypeMemNonUnitalStarSubalgebraOfT2SpaceOfIsStarNormal`, `nonUnitalCommRingTopologicalClosure`, `nonUnitalCommSemiringTopologicalClosure`, `topologicalClosure`	6
Theorems `instCompleteSpaceSubtypeMemNonUnitalStarSubalgebra`, `isClosed`, `isClosedEmbedding_coe`, `le_centralizer_centralizer`, `le_iff_mem`, `le_of_mem`, `self_mem`, `star_self_mem`, `instIsTopologicalRing`, `instIsTopologicalSemiring`, `isClosed_topologicalClosure`, `le_topologicalClosure`, `map_topologicalClosure_le`, `topologicalClosure_adjoin_le_centralizer_centralizer`, `topologicalClosure_map`, `topologicalClosure_map_le`, `topologicalClosure_minimal`	17
Total	23

NonUnitalStarAlgebra

Definitions

Name	Category	Theorems
`elemental` 📖	CompOp	14 math math: `range_cfcₙ_nnreal`, `cfcₙHom_apply_mem_elemental`, `elemental.isClosedEmbedding_coe`, `range_cfcₙHom`, `range_cfcₙ`, `elemental.isClosed`, `elemental.self_mem`, `elemental.le_centralizer_centralizer`, `elemental.star_self_mem`, `elemental.le_of_mem`, `elemental.le_iff_mem`, `cfcₙ_apply_mem_elemental`, `ContinuousMapZero.elemental_eq_top`, `elemental.instCompleteSpaceSubtypeMemNonUnitalStarSubalgebra`

NonUnitalStarAlgebra.elemental

Definitions

Name	Category	Theorems
`instNonUnitalCommRingSubtypeMemNonUnitalStarSubalgebraOfT2SpaceOfIsStarNormal` 📖	CompOp	—
`instNonUnitalCommSemiringSubtypeMemNonUnitalStarSubalgebraOfT2SpaceOfIsStarNormal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompleteSpaceSubtypeMemNonUnitalStarSubalgebra` 📖	mathematical	—	`CompleteSpace` `NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `SetLike.instMembership` `NonUnitalStarSubalgebra.instSetLike` `NonUnitalStarAlgebra.elemental` `UniformSpace.toTopologicalSpace` `instUniformSpaceSubtype`	—	`IsClosed.completeSpace_coe` `isClosed_closure`
`isClosed` 📖	mathematical	—	`IsClosed` `SetLike.coe` `NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `NonUnitalStarSubalgebra.instSetLike` `NonUnitalStarAlgebra.elemental`	—	`NonUnitalStarSubalgebra.isClosed_topologicalClosure`
`isClosedEmbedding_coe` 📖	mathematical	—	`Topology.IsClosedEmbedding` `NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `SetLike.instMembership` `NonUnitalStarSubalgebra.instSetLike` `NonUnitalStarAlgebra.elemental` `instTopologicalSpaceSubtype`	—	`Subtype.coe_injective` `Subtype.range_coe_subtype` `isClosed`
`le_centralizer_centralizer` 📖	mathematical	—	`NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalStarSubalgebra.instPartialOrder` `NonUnitalStarAlgebra.elemental` `NonUnitalStarSubalgebra.centralizer` `SetLike.coe` `NonUnitalStarSubalgebra.instSetLike` `Set` `Set.instSingletonSet`	—	`NonUnitalStarSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer`
`le_iff_mem` 📖	mathematical	—	`NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalStarSubalgebra.instPartialOrder` `NonUnitalStarAlgebra.elemental` `SetLike.instMembership` `NonUnitalStarSubalgebra.instSetLike`	—	`self_mem` `le_of_mem`
`le_of_mem` 📖	mathematical	`NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `SetLike.instMembership` `NonUnitalStarSubalgebra.instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder` `NonUnitalStarSubalgebra.instPartialOrder` `NonUnitalStarAlgebra.elemental`	—	`NonUnitalStarSubalgebra.topologicalClosure_minimal` `NonUnitalStarAlgebra.adjoin_le`
`self_mem` 📖	mathematical	—	`NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `SetLike.instMembership` `NonUnitalStarSubalgebra.instSetLike` `NonUnitalStarAlgebra.elemental`	—	`NonUnitalStarSubalgebra.le_topologicalClosure` `NonUnitalStarAlgebra.self_mem_adjoin_singleton`
`star_self_mem` 📖	mathematical	—	`NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `SetLike.instMembership` `NonUnitalStarSubalgebra.instSetLike` `NonUnitalStarAlgebra.elemental` `Star.star`	—	`NonUnitalStarSubalgebra.le_topologicalClosure` `NonUnitalStarAlgebra.star_self_mem_adjoin_singleton`

NonUnitalStarSubalgebra

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `NonUnitalStarSubalgebra` `CommRing.toCommSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `toNonUnitalRing`	—	`NonUnitalSubring.instIsTopologicalRing`
`instIsTopologicalSemiring` 📖	mathematical	—	`IsTopologicalSemiring` `NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `toNonUnitalSemiring`	—	`NonUnitalSubalgebra.instIsTopologicalSemiring`
`isClosed_topologicalClosure` 📖	mathematical	—	`IsClosed` `SetLike.coe` `NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `instSetLike` `topologicalClosure`	—	`isClosed_closure`
`le_topologicalClosure` 📖	mathematical	—	`NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`subset_closure`
`map_topologicalClosure_le` 📖	mathematical	`Continuous` `DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalStarAlgHom.instFunLike`	`NonUnitalStarSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass` `topologicalClosure`	—	`image_closure_subset_closure_image` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass`
`topologicalClosure_adjoin_le_centralizer_centralizer` 📖	mathematical	—	`NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure` `NonUnitalStarAlgebra.adjoin` `centralizer` `SetLike.coe` `instSetLike`	—	`topologicalClosure_minimal` `NonUnitalStarAlgebra.adjoin_le_centralizer_centralizer` `Set.isClosed_centralizer` `IsTopologicalSemiring.toContinuousMul`
`topologicalClosure_map` 📖	mathematical	`IsClosedMap` `DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalStarAlgHom.instFunLike` `Continuous`	`topologicalClosure` `map` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass`	—	`SetLike.coe_injective` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass` `IsClosedMap.closure_image_eq_of_continuous`
`topologicalClosure_map_le` 📖	mathematical	`IsClosedMap` `DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalStarAlgHom.instFunLike`	`NonUnitalStarSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure` `map` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `NonUnitalStarAlgHom.instStarHomClass`	—	`IsClosedMap.closure_image_subset`
`topologicalClosure_minimal` 📖	mathematical	`NonUnitalStarSubalgebra` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`topologicalClosure`	—	`closure_minimal`

---

← Back to Index