Unique

📁 Source: Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean

Statistics

Metric	Count
Definitions toNNReal, toNNReal, realContinuousMapZeroOfNNReal, realContinuousMapOfNNReal	4
Theorems instContinuousMapUniqueHom, continuous_toNNReal, toNNReal_add_add_neg_add_neg_eq, toNNReal_algebraMap, toNNReal_apply, toNNReal_mul_add_neg_mul_add_mul_neg_eq, toNNReal_neg_algebraMap, toNNReal_neg_one, toNNReal_one, continuous_toNNReal, toContinuousMapHom_toNNReal, toNNReal_add_add_neg_add_neg_eq, toNNReal_apply, toNNReal_mul_add_neg_mul_add_mul_neg_eq, toNNReal_neg_smul, toNNReal_smul, UniqueHom, UniqueHom, continuous_realContinuousMapZeroOfNNReal, map_cfcₙ, realContinuousMapZeroOfNNReal_apply, realContinuousMapZeroOfNNReal_apply_comp_toReal, realContinuousMapZeroOfNNReal_injective, map_cfcₙ, instContinuousMapUniqueHom, uniqueNonUnitalContinuousFunctionalCalculus, instContinuousMapUniqueHom, continuous_realContinuousMapOfNNReal, map_cfc, realContinuousMapOfNNReal_apply, realContinuousMapOfNNReal_apply_comp_toReal, realContinuousMapOfNNReal_injective, map_cfc	33
Total	37

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContinuousMapUniqueHom 📖	mathematical	—	ContinuousMap.UniqueHom Complex instCommSemiring instStarRing NormedField.toMetricSpace instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instContinuousStar	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing instContinuousStar RCLike.instContinuousMapUniqueHom

ContinuousMap

Definitions

Name	Category	Theorems
toNNReal 📖	CompOp	10 math math: toNNReal_neg_algebraMap, toNNReal_algebraMap, continuous_toNNReal, StarAlgHom.realContinuousMapOfNNReal_apply, toNNReal_one, toNNReal_mul_add_neg_mul_add_mul_neg_eq, ContinuousMapZero.toContinuousMapHom_toNNReal, toNNReal_apply, toNNReal_neg_one, toNNReal_add_add_neg_add_neg_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_toNNReal 📖	mathematical	—	Continuous ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal NNReal.instTopologicalSpace compactOpen toNNReal	—	continuous_postcomp
toNNReal_add_add_neg_add_neg_eq 📖	mathematical	—	ContinuousMap NNReal NNReal.instTopologicalSpace instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring toNNReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instNegOfContinuousNeg Real.instNeg IsTopologicalRing.toContinuousNeg	—	ext IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalRing.toContinuousNeg NNReal.eq max_neg_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero
toNNReal_algebraMap 📖	mathematical	—	toNNReal DFunLike.coe RingHom Real ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Semiring.toNonAssocSemiring CommSemiring.toSemiring Real.instCommSemiring instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal RingHom.instFunLike algebraMap algebra Algebra.id NNReal.toReal NNReal NNReal.instTopologicalSpace instCommSemiringNNReal instSemiringNNReal NNReal.instIsTopologicalSemiring	—	ext IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal NNReal.instIsTopologicalSemiring NNReal.eq algebraMap_apply mul_one Real.toNNReal_coe
toNNReal_apply 📖	mathematical	—	DFunLike.coe ContinuousMap NNReal NNReal.instTopologicalSpace instFunLike toNNReal Real.toNNReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	—
toNNReal_mul_add_neg_mul_add_mul_neg_eq 📖	mathematical	—	ContinuousMap NNReal NNReal.instTopologicalSpace instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring toNNReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instMul Real.instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Distrib.toMul instNegOfContinuousNeg Real.instNeg IsTopologicalRing.toContinuousNeg	—	ext IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalRing.toContinuousNeg NNReal.eq max_neg_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_mul Distrib.rightDistribClass neg_mul mul_add Distrib.leftDistribClass mul_neg neg_add_rev neg_neg Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Abel.zero_termg
toNNReal_neg_algebraMap 📖	mathematical	—	toNNReal ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instNegOfContinuousNeg Real.instNeg IsTopologicalRing.toContinuousNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Real.instCommSemiring instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring RingHom.instFunLike algebraMap algebra Algebra.id NNReal.toReal NNReal NNReal.instTopologicalSpace instZero instZeroNNReal	—	ext IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal IsTopologicalRing.toIsTopologicalSemiring NNReal.eq algebraMap_apply mul_one sup_of_le_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
toNNReal_neg_one 📖	mathematical	—	toNNReal ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instNegOfContinuousNeg Real.instNeg IsTopologicalRing.toContinuousNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instOne Real.instOne NNReal NNReal.instTopologicalSpace instZero instZeroNNReal	—	toNNReal_neg_algebraMap
toNNReal_one 📖	mathematical	—	toNNReal ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instOne Real.instOne NNReal NNReal.instTopologicalSpace instOneNNReal	—	toNNReal_algebraMap

ContinuousMapZero

Definitions

Name	Category	Theorems
toNNReal 📖	CompOp	8 math math: NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply, toNNReal_mul_add_neg_mul_add_mul_neg_eq, toContinuousMapHom_toNNReal, toNNReal_add_add_neg_add_neg_eq, toNNReal_neg_smul, toNNReal_smul, continuous_toNNReal, toNNReal_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_toNNReal 📖	mathematical	—	Continuous ContinuousMapZero Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal instZeroNNReal NNReal.instTopologicalSpace instTopologicalSpace toNNReal	—	instContinuousMapClass continuous_induced_rng Continuous.comp ContinuousMap.continuous_postcomp continuous_induced_dom
toContinuousMapHom_toNNReal 📖	mathematical	—	ContinuousMap.toNNReal DFunLike.coe NonUnitalStarAlgHom Real ContinuousMapZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Real.instCommSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring instNonUnitalCommSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal Module.toDistribMulAction instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsTopologicalSemiring.toContinuousAdd instModule Semiring.toModule SMulCommClass.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Algebra.to_smulCommClass Algebra.id IsTopologicalSemiring.toContinuousMul Semiring.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid instStarRing instStarRingReal instContinuousStarReal ContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring ContinuousMap.instDistribMulActionOfContinuousConstSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne ContinuousMap.instStar NonUnitalStarAlgHom.instFunLike toContinuousMapHom NNReal instCommSemiringNNReal NNReal.instTopologicalSpace NNReal.instIsTopologicalSemiring instStarRingNNReal NNReal.instContinuousStar toNNReal	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul instContinuousStarReal
toNNReal_add_add_neg_add_neg_eq 📖	mathematical	—	ContinuousMapZero NNReal instZeroNNReal NNReal.instTopologicalSpace instAdd AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring NNReal.instIsTopologicalSemiring toNNReal Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instAddCommGroup IsTopologicalRing.toContinuousNeg	—	toContinuousMap_injective IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalRing.toContinuousNeg instContinuousMapClass SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul NNReal.instContinuousStar map_add SemilinearMapClass.toAddHomClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul NonUnitalAlgHomClass.instLinearMapClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass ContinuousMap.toNNReal_add_add_neg_add_neg_eq
toNNReal_apply 📖	mathematical	—	DFunLike.coe ContinuousMapZero NNReal instZeroNNReal NNReal.instTopologicalSpace instFunLike toNNReal Real.toNNReal Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	—
toNNReal_mul_add_neg_mul_add_mul_neg_eq 📖	mathematical	—	ContinuousMapZero NNReal instZeroNNReal NNReal.instTopologicalSpace instAdd AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring NNReal.instIsTopologicalSemiring toNNReal Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instMul NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instAddCommGroup IsTopologicalRing.toContinuousNeg	—	toContinuousMap_injective IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalRing.toContinuousNeg instContinuousMapClass SMulCommClass.continuousConstSMul Algebra.to_smulCommClass NNReal.instContinuousStar map_add SemilinearMapClass.toAddHomClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul NonUnitalAlgHomClass.instLinearMapClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass ContinuousMap.toNNReal_mul_add_neg_mul_add_mul_neg_eq
toNNReal_neg_smul 📖	mathematical	—	toNNReal ContinuousMapZero Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instAddCommGroup IsTopologicalRing.toContinuousNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal NNReal instSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass Real.instAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NNReal.instDistribMulActionOfReal Module.toDistribMulAction Real.semiring Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace SMulCommClass.continuousConstSMul Real.instMonoid SMulZeroClass.toSMul Algebra.to_smulCommClass instCommSemiringNNReal NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring instZeroNNReal NNReal.instTopologicalSpace AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring UniformContinuousConstSMul.to_continuousConstSMul instPseudoMetricSpaceNNReal IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul	—	IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul IsTopologicalSemiring.toContinuousAdd Ring.uniformContinuousConstSMul instIsUniformAddGroupReal NNReal.smul_def instIsTopologicalAddGroupReal smul_neg toNNReal_smul
toNNReal_smul 📖	mathematical	—	toNNReal NNReal ContinuousMapZero Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass Real.instAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NNReal.instDistribMulActionOfReal Module.toDistribMulAction Real.semiring Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace SMulCommClass.continuousConstSMul Real.instMonoid SMulZeroClass.toSMul Algebra.to_smulCommClass instCommSemiringNNReal NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal instZeroNNReal NNReal.instTopologicalSpace AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring UniformContinuousConstSMul.to_continuousConstSMul instPseudoMetricSpaceNNReal IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul	—	ext SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul NNReal.eq max_eq_left mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing NNReal.coe_nonneg max_eq_right LT.lt.le MulZeroClass.mul_zero mul_nonpos_of_nonneg_of_nonpos

NNReal.instContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
UniqueHom 📖	mathematical	—	ContinuousMap.UniqueHom NNReal instCommSemiringNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instAlgebraOfReal Ring.toSemiring	—	NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Real.toNNReal_coe NNReal.eq NNReal.coe_nonneg Continuous.subtype_map NNReal.continuous_coe continuous_real_toNNReal IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Homeomorph.instContinuousMapClass Continuous.comp StarAlgHom.continuous_realContinuousMapOfNNReal ContinuousMap.continuous_precomp StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal Homeomorph.compactSpace ContinuousMap.UniqueHom.eq_of_continuous_of_map_id Real.instContinuousMapUniqueHom StarAlgHom.ext Homeomorph.symm_comp_toContinuousMap ContinuousMap.comp_id StarAlgHom.realContinuousMapOfNNReal_injective StarAlgHom.comp_id

NNReal.instContinuousMapZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
UniqueHom 📖	mathematical	—	ContinuousMapZero.UniqueHom NNReal instCommSemiringNNReal instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real Real.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left	—	NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul Real.toNNReal_coe NNReal.eq NNReal.coe_nonneg Continuous.subtype_map NNReal.continuous_coe continuous_real_toNNReal Fact.out NNReal.coe_zero Homeomorph.symm_apply_apply UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Ring.uniformContinuousConstSMul instIsUniformAddGroupReal Homeomorph.instContinuousMapClass Continuous.comp NonUnitalStarAlgHom.continuous_realContinuousMapZeroOfNNReal ContinuousMapZero.instContinuousMapClass continuous_induced_rng ContinuousMap.continuous_precomp continuous_induced_dom NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal Homeomorph.compactSpace RCLike.uniqueNonUnitalContinuousFunctionalCalculus ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id NonUnitalStarAlgHom.ext ContinuousMapZero.ext NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective NonUnitalStarAlgHom.comp_id

NonUnitalStarAlgHom

Definitions

Name	Category	Theorems
realContinuousMapZeroOfNNReal 📖	CompOp	4 math math: realContinuousMapZeroOfNNReal_apply_comp_toReal, realContinuousMapZeroOfNNReal_apply, realContinuousMapZeroOfNNReal_injective, continuous_realContinuousMapZeroOfNNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_realContinuousMapZeroOfNNReal 📖	mathematical	Continuous ContinuousMapZero NNReal instZeroNNReal NNReal.instTopologicalSpace ContinuousMapZero.instTopologicalSpace DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring instCommSemiringNNReal NNReal.instIsTopologicalSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsTopologicalSemiring.toContinuousAdd ContinuousMapZero.instModule Semiring.toModule UniformContinuousConstSMul.to_continuousConstSMul PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid ContinuousMapZero.instStarRing instStarRingNNReal NNReal.instContinuousStar NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NNReal.instDistribMulActionOfReal Real Real.semiring instFunLike	Real.instZero UniformSpace.toTopologicalSpace Real.pseudoMetricSpace Real.instMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing ContinuousMapZero.instNonUnitalCommRing Real.commRing instIsTopologicalRingReal Real.instAddCommMonoid NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Real.instCommSemiring instStarRingReal instContinuousStarReal realContinuousMapZeroOfNNReal	—	NNReal.instIsTopologicalSemiring IsTopologicalSemiring.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul NNReal.instContinuousStar instIsTopologicalRingReal IsTopologicalRing.toIsTopologicalSemiring Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul instContinuousStarReal Continuous.sub IsTopologicalAddGroup.to_continuousSub IsTopologicalRing.to_topologicalAddGroup Continuous.comp' ContinuousMapZero.continuous_toNNReal Continuous.neg ContinuousMapZero.instContinuousNeg continuous_id'
map_cfcₙ 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Continuous DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommRing.toCommSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid instFunLike	cfcₙ	—	NonUnitalStarAlgHomClass.map_cfcₙ instNonUnitalAlgHomClass instStarHomClass
realContinuousMapZeroOfNNReal_apply 📖	mathematical	—	DFunLike.coe NonUnitalStarAlgHom Real ContinuousMapZero Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing ContinuousMapZero.instNonUnitalCommRing Real.commRing instIsTopologicalRingReal Module.toDistribMulAction Real.semiring ContinuousMapZero.instAddCommMonoid Real.instAddCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring ContinuousMapZero.instModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing Real.instCommSemiring instStarRingReal instContinuousStarReal NonUnitalRing.toNonUnitalNonAssocRing instFunLike realContinuousMapZeroOfNNReal SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NNReal instZeroNNReal NNReal.instTopologicalSpace instSemiringNNReal NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring instCommSemiringNNReal NNReal.instIsTopologicalSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instStarRingNNReal NNReal.instContinuousStar NNReal.instDistribMulActionOfReal ContinuousMapZero.toNNReal ContinuousMapZero.instNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instAddCommGroup	—	NNReal.instIsTopologicalSemiring IsTopologicalSemiring.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul NNReal.instContinuousStar instIsTopologicalRingReal IsTopologicalRing.toIsTopologicalSemiring Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul instContinuousStarReal
realContinuousMapZeroOfNNReal_apply_comp_toReal 📖	mathematical	—	DFunLike.coe NonUnitalStarAlgHom Real ContinuousMapZero Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing ContinuousMapZero.instNonUnitalCommRing Real.commRing instIsTopologicalRingReal Module.toDistribMulAction Real.semiring ContinuousMapZero.instAddCommMonoid Real.instAddCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring ContinuousMapZero.instModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing Real.instCommSemiring instStarRingReal instContinuousStarReal NonUnitalRing.toNonUnitalNonAssocRing instFunLike realContinuousMapZeroOfNNReal ContinuousMapZero.comp NNReal instZeroNNReal NNReal.instTopologicalSpace NNReal.toReal NNReal.continuous_coe ContinuousMap ContinuousMap.instFunLike instSemiringNNReal NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring instCommSemiringNNReal NNReal.instIsTopologicalSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instPseudoMetricSpaceNNReal IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul instStarRingNNReal NNReal.instContinuousStar NNReal.instDistribMulActionOfReal	—	NNReal.instIsTopologicalSemiring IsTopologicalSemiring.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul NNReal.instContinuousStar instIsTopologicalRingReal IsTopologicalRing.toIsTopologicalSemiring Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul instContinuousStarReal NNReal.continuous_coe ContinuousMapZero.ext NNReal.eq Real.toNNReal_coe sup_of_le_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgHomClass sub_zero
realContinuousMapZeroOfNNReal_injective 📖	mathematical	—	NonUnitalStarAlgHom NNReal ContinuousMapZero instZeroNNReal NNReal.instTopologicalSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring instCommSemiringNNReal NNReal.instIsTopologicalSemiring Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsTopologicalSemiring.toContinuousAdd ContinuousMapZero.instModule Semiring.toModule UniformContinuousConstSMul.to_continuousConstSMul PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid ContinuousMapZero.instStarRing instStarRingNNReal NNReal.instContinuousStar NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NNReal.instDistribMulActionOfReal Real Real.semiring Real.instZero UniformSpace.toTopologicalSpace Real.pseudoMetricSpace Real.instMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing ContinuousMapZero.instNonUnitalCommRing Real.commRing instIsTopologicalRingReal Real.instAddCommMonoid NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Real.instCommSemiring instStarRingReal instContinuousStarReal realContinuousMapZeroOfNNReal	—	NNReal.instIsTopologicalSemiring IsTopologicalSemiring.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul NNReal.instContinuousStar instIsTopologicalRingReal IsTopologicalRing.toIsTopologicalSemiring Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul instContinuousStarReal ext NNReal.continuous_coe realContinuousMapZeroOfNNReal_apply_comp_toReal

NonUnitalStarAlgHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_cfcₙ 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace quasispectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Continuous DFunLike.coe	cfcₙ	—	NonUnitalAlgHom.quasispectrum_apply_subset' Continuous.subtype_map continuous_id IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum instFactMemSetQuasispectrumOfNat Continuous.comp' cfcₙHom_continuous ContinuousMapZero.continuous_comp_left cfcₙHom_id ContinuousOn.mono ContinuousOn.restrict cfcₙ_apply DFunLike.congr_fun

RCLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContinuousMapUniqueHom 📖	mathematical	—	ContinuousMap.UniqueHom Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instContinuousStar	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing instContinuousStar ContinuousMap.starAlgHom_ext_map_X ContinuousMap.ext Polynomial.eval_X
uniqueNonUnitalContinuousFunctionalCalculus 📖	mathematical	—	ContinuousMapZero.UniqueHom Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instContinuousStar	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing instContinuousStar IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul DFunLike.ext'_iff Set.eqOn_univ UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup ContinuousMapZero.instIsScalarTower' IsScalarTower.right ContinuousMapZero.instSMulCommClass' ContinuousMapZero.instStarModule StarMul.toStarModule Dense.closure_eq ContinuousMapZero.adjoin_id_dense Set.EqOn.closure NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass NonUnitalStarAlgHom.mem_equalizer NonUnitalStarAlgebra.adjoin_le Set.singleton_subset_iff

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContinuousMapUniqueHom 📖	mathematical	—	ContinuousMap.UniqueHom Real instCommSemiring instStarRingReal metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing normedCommRing instIsTopologicalRingReal instContinuousStarReal	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal RCLike.instContinuousMapUniqueHom

StarAlgHom

Definitions

Name	Category	Theorems
realContinuousMapOfNNReal 📖	CompOp	4 math math: continuous_realContinuousMapOfNNReal, realContinuousMapOfNNReal_apply, realContinuousMapOfNNReal_apply_comp_toReal, realContinuousMapOfNNReal_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_realContinuousMapOfNNReal 📖	mathematical	Continuous ContinuousMap NNReal NNReal.instTopologicalSpace ContinuousMap.compactOpen DFunLike.coe StarAlgHom instCommSemiringNNReal ContinuousMap.instSemiringOfIsTopologicalSemiring instSemiringNNReal NNReal.instIsTopologicalSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid instStarRingNNReal NNReal.instContinuousStar Ring.toSemiring NNReal.instAlgebraOfReal NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instFunLike	Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instCommSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instStarRingReal instContinuousStarReal realContinuousMapOfNNReal	—	NNReal.instIsTopologicalSemiring NNReal.instContinuousStar IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Continuous.sub IsTopologicalAddGroup.to_continuousSub IsTopologicalRing.to_topologicalAddGroup Continuous.comp' ContinuousMap.continuous_toNNReal Continuous.neg IsTopologicalAddGroup.toContinuousNeg instIsTopologicalAddGroupReal ContinuousMap.instIsTopologicalAddGroup continuous_id'
map_cfc 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum Continuous DFunLike.coe StarAlgHom Ring.toSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid instFunLike	cfc	—	StarAlgHomClass.map_cfc instAlgHomClass instStarHomClass
realContinuousMapOfNNReal_apply 📖	mathematical	—	DFunLike.coe StarAlgHom Real ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instCommSemiring ContinuousMap.instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid instStarRingReal instContinuousStarReal Ring.toSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instFunLike realContinuousMapOfNNReal SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne NNReal NNReal.instTopologicalSpace instCommSemiringNNReal instSemiringNNReal NNReal.instIsTopologicalSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instStarRingNNReal NNReal.instContinuousStar NNReal.instAlgebraOfReal ContinuousMap.toNNReal ContinuousMap.instNegOfContinuousNeg Real.instNeg	—	NNReal.instIsTopologicalSemiring NNReal.instContinuousStar IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal
realContinuousMapOfNNReal_apply_comp_toReal 📖	mathematical	—	DFunLike.coe StarAlgHom Real ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instCommSemiring ContinuousMap.instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid instStarRingReal instContinuousStarReal Ring.toSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instFunLike realContinuousMapOfNNReal ContinuousMap.comp NNReal NNReal.instTopologicalSpace NNReal.toReal NNReal.continuous_coe instCommSemiringNNReal instSemiringNNReal NNReal.instIsTopologicalSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instStarRingNNReal NNReal.instContinuousStar NNReal.instAlgebraOfReal	—	NNReal.instIsTopologicalSemiring NNReal.instContinuousStar IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.continuous_coe ContinuousMap.ext NNReal.eq Real.toNNReal_coe sup_of_le_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass instAlgHomClass sub_zero
realContinuousMapOfNNReal_injective 📖	mathematical	—	StarAlgHom NNReal ContinuousMap NNReal.instTopologicalSpace instCommSemiringNNReal ContinuousMap.instSemiringOfIsTopologicalSemiring instSemiringNNReal NNReal.instIsTopologicalSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid instStarRingNNReal NNReal.instContinuousStar Ring.toSemiring NNReal.instAlgebraOfReal NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instCommSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instStarRingReal instContinuousStarReal realContinuousMapOfNNReal	—	NNReal.instIsTopologicalSemiring NNReal.instContinuousStar IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal ext NNReal.continuous_coe realContinuousMapOfNNReal_apply_comp_toReal

StarAlgHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_cfc 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum Continuous DFunLike.coe	cfc	—	AlgHom.spectrum_apply_subset StarAlgHom.instAlgHomClass Continuous.subtype_map continuous_id ContinuousMap.UniqueHom.eq_of_continuous_of_map_id ContinuousFunctionalCalculus.compactSpace_spectrum Continuous.comp' cfcHom_continuous ContinuousMap.continuous_precomp cfcHom_id ContinuousOn.mono ContinuousOn.restrict cfc_apply

---

← Back to Index