Documentation Verification Report

Star

📁 Source: Mathlib/Topology/ContinuousMap/Bounded/Star.lean

Statistics

Metric	Count
Definitions `instStarAddMonoid`, `instStarRing`, `toContinuousMapStarₐ`	3
Theorems `coe_star`, `coe_toContinuousMapStarₐ`, `instCStarRing`, `instNormedStarGroup`, `instStarModule`, `star_apply`, `toContinuousMapStarₐ_apply_apply`	7
Total	10

BoundedContinuousFunction

Definitions

Name	Category	Theorems
`instStarAddMonoid` 📖	CompOp	9 math math: `mkOfCompact_star`, `char_neg`, `coe_toContinuousMapStarₐ`, `instStarModule`, `instNormedStarGroup`, `toContinuousMapStarₐ_apply_apply`, `star_mem_range_charAlgHom`, `star_apply`, `coe_star`
`instStarRing` 📖	CompOp	5 math math: `mem_charPoly`, `instCStarRing`, `separatesPoints_charPoly`, `RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict`, `char_mem_charPoly`
`toContinuousMapStarₐ` 📖	CompOp	4 math math: `coe_toContinuousMapStarₐ`, `toContinuousMapStarₐ_apply_apply`, `separatesPoints_charPoly`, `RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_star` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instFunLike` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instStarAddMonoid` `Pi.instStarForall`	—	`instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`coe_toContinuousMapStarₐ` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ContinuousMap.instFunLike` `StarAlgHom` `BoundedContinuousFunction` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `instSemiring` `Ring.toSemiring` `NormedRing.toRing` `instBoundedMul` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `instAlgebra` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instStarAddMonoid` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.algebra` `NormedAlgebra.toAlgebra` `ContinuousMap.instStar` `NormedStarGroup.to_continuousStar` `StarAlgHom.instFunLike` `toContinuousMapStarₐ` `instFunLike`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NormedStarGroup.to_continuousStar`
`instCStarRing` 📖	mathematical	—	`CStarRing` `BoundedContinuousFunction` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `instNonUnitalNormedRing` `instStarRing` `CStarRing.to_normedStarGroup`	—	`CStarRing.to_normedStarGroup` `sq` `Real.le_sqrt` `norm_nonneg` `norm_le` `Real.sqrt_nonneg` `CStarRing.norm_star_mul_self` `norm_coe_le_norm` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`instNormedStarGroup` 📖	mathematical	—	`NormedStarGroup` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instSeminormedAddCommGroup` `instStarAddMonoid`	—	`norm_eq` `norm_star`
`instStarModule` 📖	mathematical	—	`StarModule` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `StarRing.toStarAddMonoid` `instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instStarAddMonoid` `instSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `NormedSpace.toIsBoundedSMul`	—	`instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NormedSpace.toIsBoundedSMul` `ext` `StarModule.star_smul`
`star_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `instFunLike` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instStarAddMonoid`	—	`instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`toContinuousMapStarₐ_apply_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ContinuousMap.instFunLike` `StarAlgHom` `BoundedContinuousFunction` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `instSemiring` `Ring.toSemiring` `NormedRing.toRing` `instBoundedMul` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `instAlgebra` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instStarAddMonoid` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.algebra` `NormedAlgebra.toAlgebra` `ContinuousMap.instStar` `NormedStarGroup.to_continuousStar` `StarAlgHom.instFunLike` `toContinuousMapStarₐ` `instFunLike`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NormedStarGroup.to_continuousStar`

---

← Back to Index