Isometric

📁 Source: Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Isometric.lean

Statistics

Metric	Count
Definitions	0
Theorems norm_negPart_le, norm_posPart_le, norm_eq_max_norm_posPart_negPart	3
Total	3

CStarAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_negPart_le 📖	mathematical	—	Real Real.instLE Norm.norm NonUnitalNormedRing.toNorm NegPart.negPart instNegPart NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus CFC.posPart_neg TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace norm_neg norm_posPart_le
norm_posPart_le 📖	mathematical	—	Real Real.instLE Norm.norm NonUnitalNormedRing.toNorm PosPart.posPart instPosPart NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus norm_cfcₙ_le le_or_gt max_eq_right norm_zero max_eq_left LT.lt.le NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le cfcₙ_apply_of_not_predicate

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_eq_max_norm_posPart_negPart 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing StarRing.toStarAddMonoid	Norm.norm NonUnitalNormedRing.toNorm Real Real.instMax PosPart.posPart CStarAlgebra.instPosPart NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalNormedRing.toMetricSpace NegPart.negPart CStarAlgebra.instNegPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal le_antisymm NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus cfcₙ_id' IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar norm_cfcₙ_le_iff continuousOn_id' le_total le_max_of_le_left posPart_eq_self norm_apply_le_norm_cfcₙ Continuous.continuousOn continuous_posPart instHasSolidNormReal Real.instIsOrderedAddMonoid posPart_zero le_max_of_le_right negPart_eq_neg IsOrderedAddMonoid.toAddLeftMono norm_neg continuous_negPart negPart_of_nonpos neg_zero max_le CStarAlgebra.norm_posPart_le CStarAlgebra.norm_negPart_le

---

← Back to Index