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 instPartialOrderNNReal instZeroNNReal instOneNNReal	Monotone 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 IsStarNormal.instNonUnitalContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass'	—	SMulCommClass.complexToReal NonUnitalCStarAlgebra.toSMulCommClass IsScalarTower.complexToReal NonUnitalCStarAlgebra.toIsScalarTower IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus IsStarNormal.instNonUnitalContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass' LE.le.trans Set.ext NNReal.instCanonicallyOrderedAdd Set.union_singleton Set.Ioo_insert_left instZeroLEOneClass NNReal.instStarOrderedRing NeZero.charZero_one IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing Set.Ico_insert_right nnrpow_zero 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 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 IsStarNormal.instContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass' CStarAlgebra.toNonUnitalCStarAlgebra	—	IsSelfAdjoint.instContinuousFunctionalCalculus IsStarNormal.instContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass' LE.le.lt_or_eq' zero_le NNReal.instCanonicallyOrderedAdd Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace nnrpow_eq_rpow NonUnitalSeminormedRing.toIsTopologicalRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace monotone_nnrpow LE.le.trans rpow_zero 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 IsStarNormal.instNonUnitalContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass'	—	SMulCommClass.complexToReal NonUnitalCStarAlgebra.toSMulCommClass IsScalarTower.complexToReal NonUnitalCStarAlgebra.toIsScalarTower IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus IsStarNormal.instNonUnitalContinuousFunctionalCalculus 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 NNReal.instIsStrictOrderedRing NNReal.instCanonicallyOrderedAdd PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono Mathlib.Meta.NormNum.isNat_le_true NNReal.instIsOrderedRing Nat.cast_zero
nnrpow_le_nnrpow 📖	mathematical	NNReal Set Set.instMembership Set.Icc PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal instOneNNReal Preorder.toLE	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 IsStarNormal.instNonUnitalContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass'	—	monotone_nnrpow
rpow_le_rpow 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne Preorder.toLE PartialOrder.toPreorder	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 IsStarNormal.instContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass' CStarAlgebra.toNonUnitalCStarAlgebra	—	monotone_rpow
sqrt_le_sqrt 📖	mathematical	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 IsStarNormal.instNonUnitalContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass'	—	monotone_sqrt

---

← Back to Index