Order

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

Statistics

Metric	Count
Definitions	0
Theorems monotone_nnrpow, monotone_rpow, monotone_sqrt, nnrpow_le_nnrpow, rpow_le_rpow, sqrt_le_sqrt	6
Total	6

CFC

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
monotone_nnrpow 📖	mathematical	NNReal Set Set.instMembership Set.Icc PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero NNReal.instOne	Monotone PartialOrder.toPreorder NNReal instPowNNReal NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toStarRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NormedSpace.complexToReal NonUnitalCStarAlgebra.toNormedSpace SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup Complex Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalCStarAlgebra.toSMulCommClass IsScalarTower.complexToReal NonUnitalCStarAlgebra.toIsScalarTower IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NonUnitalNormedRing.toMetricSpace IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass'	—	SMulCommClass.complexToReal NonUnitalCStarAlgebra.toSMulCommClass IsScalarTower.complexToReal NonUnitalCStarAlgebra.toIsScalarTower IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass' LE.le.trans Set.ext Set.union_singleton Set.Ioo_insert_left instZeroLEOneClass NNReal.instStarOrderedRing NeZero.charZero_one IsStrictOrderedRing.toCharZero Set.Ico_insert_right nnrpow_zero instReflLe nnrpow_one cfcₙ_apply_of_not_predicate NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instNonUnitalContinuousFunctionalCalculus
monotone_rpow 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	Monotone PartialOrder.toPreorder Real instPowReal NormedRing.toRing CStarAlgebra.toNormedRing CStarAlgebra.toStarRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedAlgebra.toAlgebra Real.normedField NormedAlgebra.complexToReal CStarAlgebra.toNormedAlgebra IsSelfAdjoint.instContinuousFunctionalCalculus Complex Complex.instNormedField IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NormedRing.toMetricSpace IsStarNormal.instIsometricContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass' CStarAlgebra.toNonUnitalCStarAlgebra	—	IsSelfAdjoint.instContinuousFunctionalCalculus IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar IsStarNormal.instIsometricContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass' LE.le.lt_or_eq' zero_le Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital instIsTopologicalRingReal instContinuousStarReal nnrpow_eq_rpow IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace monotone_nnrpow LE.le.trans rpow_zero instReflLe cfc_apply_of_not_predicate NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus
monotone_sqrt 📖	mathematical	—	Monotone PartialOrder.toPreorder sqrt NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toStarRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NormedSpace.complexToReal NonUnitalCStarAlgebra.toNormedSpace SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup Complex Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalCStarAlgebra.toSMulCommClass IsScalarTower.complexToReal NonUnitalCStarAlgebra.toIsScalarTower IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NonUnitalNormedRing.toMetricSpace IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass'	—	SMulCommClass.complexToReal NonUnitalCStarAlgebra.toSMulCommClass IsScalarTower.complexToReal NonUnitalCStarAlgebra.toIsScalarTower IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass' Nat.instAtLeastTwoHAddOfNat sqrt_eq_nnrpow monotone_nnrpow Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono Mathlib.Meta.NormNum.isNat_le_true Nat.cast_zero
nnrpow_le_nnrpow 📖	mathematical	NNReal Set Set.instMembership Set.Icc PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero NNReal.instOne Preorder.toLE	Preorder.toLE PartialOrder.toPreorder NNReal instPowNNReal NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toStarRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NormedSpace.complexToReal NonUnitalCStarAlgebra.toNormedSpace SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup Complex Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalCStarAlgebra.toSMulCommClass IsScalarTower.complexToReal NonUnitalCStarAlgebra.toIsScalarTower IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NonUnitalNormedRing.toMetricSpace IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass'	—	monotone_nnrpow
rpow_le_rpow 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne Preorder.toLE PartialOrder.toPreorder	Preorder.toLE PartialOrder.toPreorder Real instPowReal NormedRing.toRing CStarAlgebra.toNormedRing CStarAlgebra.toStarRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedAlgebra.toAlgebra Real.normedField NormedAlgebra.complexToReal CStarAlgebra.toNormedAlgebra IsSelfAdjoint.instContinuousFunctionalCalculus Complex Complex.instNormedField IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NormedRing.toMetricSpace IsStarNormal.instIsometricContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass' CStarAlgebra.toNonUnitalCStarAlgebra	—	monotone_rpow
sqrt_le_sqrt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLE PartialOrder.toPreorder sqrt NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toStarRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NormedSpace.complexToReal NonUnitalCStarAlgebra.toNormedSpace SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup Complex Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalCStarAlgebra.toSMulCommClass IsScalarTower.complexToReal NonUnitalCStarAlgebra.toIsScalarTower IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NonUnitalNormedRing.toMetricSpace IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass'	—	monotone_sqrt

---

← Back to Index