Isometric

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

Statistics

Metric	Count
Definitions	0
Theorems continuousOn_nnrpow, continuousOn_rpow, continuousOn_sqrt, nnnorm_nnrpow, nnnorm_rpow, nnnorm_sqrt, norm_nnrpow, norm_rpow, norm_sqrt	9
Total	9

CFC

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_nnrpow 📖	mathematical	—	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NNReal instPowNNReal NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup 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 setOf Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus eq_zero_or_pos NNReal.instCanonicallyOrderedAdd nnrpow_zero continuousOn_const ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace NonUnitalSeminormedRing.toIsTopologicalRing Filter.univ_mem continuousOn_id NNReal.continuousOn_rpow_const
continuousOn_rpow 📖	mathematical	—	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Real instPowReal NormedRing.toRing NormedAlgebra.toAlgebra Real.normedField IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace setOf IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal ContinuousOn.cfc_nnreal_of_mem_nhdsSet TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace NonUnitalSeminormedRing.toIsTopologicalRing nhdsSet_iUnion IsOpen.mem_nhdsSet isOpen_compl_singleton T5Space.toT1Space OrderTopology.t5Space NNReal.instOrderTopology spectrum.zero_notMem IsStrictlyPositive.isUnit continuousOn_id IsStrictlyPositive.nonneg NNReal.continuousOn_rpow_const
continuousOn_sqrt 📖	mathematical	—	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing sqrt NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup 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 setOf Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace NonUnitalSeminormedRing.toIsTopologicalRing Filter.univ_mem continuousOn_id Continuous.continuousOn NNReal.continuous_sqrt NNReal.sqrt_zero
nnnorm_nnrpow 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing instPowNNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NormedSpace.toModule Real Real.normedField NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid 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 NNReal.instPowReal NNReal.toReal	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal MonotoneOn.nnnorm_cfcₙ Monotone.monotoneOn NNReal.monotone_nnrpow_const NNReal.continuousOn_rpow_const
nnnorm_rpow 📖	mathematical	Real Real.instLT Real.instZero Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing instPowReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedAlgebra.toAlgebra Real.normedField IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace NNReal NNReal.instPowReal	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus CanLift.prf NNReal.canLift LT.lt.le Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace nnrpow_eq_rpow NonUnitalSeminormedRing.toIsTopologicalRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus Real.instNontrivial IsometricContinuousFunctionalCalculus.toNonUnital nnnorm_nnrpow
nnnorm_sqrt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing sqrt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NormedSpace.toModule Real Real.normedField NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid 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 DFunLike.coe OrderIso NNReal instPartialOrderNNReal instFunLikeOrderIso NNReal.sqrt	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus Nat.instAtLeastTwoHAddOfNat sqrt_eq_nnrpow NNReal.sqrt_eq_rpow nnnorm_nnrpow one_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono NNReal.instIsOrderedRing
norm_nnrpow 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	Norm.norm NonUnitalNormedRing.toNorm instPowNNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid 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.instPow NNReal.toReal	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus nnnorm_nnrpow
norm_rpow 📖	mathematical	Real Real.instLT Real.instZero Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	Norm.norm NormedRing.toNorm instPowReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedAlgebra.toAlgebra Real.normedField IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace Real.instPow	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus nnnorm_rpow
norm_sqrt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	Norm.norm NonUnitalNormedRing.toNorm sqrt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid 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.sqrt	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus Real.coe_sqrt nnnorm_sqrt

---

← Back to Index