Real

📁 Source: Mathlib/Data/ENNReal/Real.lean

Statistics

Metric	Count
Definitions `toNNRealHom`, `toRealHom`, `evalENNRealOfReal`	3
Theorems `coe_lt_ofReal`, `dichotomy`, `le_ofReal_iff_toReal_le`, `le_toNNReal_of_coe_le`, `lt_ofReal_iff_toReal_lt`, `natCast_le_ofReal`, `natCast_lt_ofReal`, `ofNat_le_ofReal`, `ofNat_lt_ofReal`, `ofReal_add`, `ofReal_add_le`, `ofReal_eq_natCast`, `ofReal_eq_ofNat`, `ofReal_eq_ofReal_iff`, `ofReal_eq_one`, `ofReal_eq_zero`, `ofReal_le_coe`, `ofReal_le_iff_le_toReal`, `ofReal_le_natCast`, `ofReal_le_ofNat`, `ofReal_le_ofReal`, `ofReal_le_ofReal_iff`, `ofReal_le_ofReal_iff'`, `ofReal_le_of_le_toReal`, `ofReal_le_one`, `ofReal_lt_coe_iff`, `ofReal_lt_iff_lt_toReal`, `ofReal_lt_natCast`, `ofReal_lt_ofNat`, `ofReal_lt_ofReal_iff`, `ofReal_lt_ofReal_iff'`, `ofReal_lt_ofReal_iff_of_nonneg`, `ofReal_lt_one`, `ofReal_max`, `ofReal_min`, `ofReal_mono`, `ofReal_mul`, `ofReal_mul'`, `ofReal_ne_zero_iff`, `ofReal_nsmul`, `ofReal_of_nonpos`, `ofReal_pos`, `ofReal_pow`, `one_le_ofReal`, `one_lt_ofReal`, `sup_eq_zero`, `toNNReal_le_toNNReal`, `toNNReal_lt_of_lt_coe`, `toNNReal_lt_toNNReal`, `toNNReal_mono`, `toNNReal_mul`, `toNNReal_mul_top`, `toNNReal_pos`, `toNNReal_pos_iff`, `toNNReal_pow`, `toNNReal_strict_mono`, `toNNReal_top_mul`, `toReal_add`, `toReal_add_le`, `toReal_eq_toReal`, `toReal_inf`, `toReal_le_of_le_ofReal`, `toReal_le_toReal`, `toReal_lt_of_lt_ofReal`, `toReal_lt_toReal`, `toReal_max`, `toReal_min`, `toReal_mono`, `toReal_mono'`, `toReal_mul`, `toReal_mul_top`, `toReal_nsmul`, `toReal_ofReal_mul`, `toReal_pos`, `toReal_pos_iff`, `toReal_pos_iff_ne_top`, `toReal_pow`, `toReal_strict_mono`, `toReal_sup`, `toReal_top_mul`, `trichotomy`, `trichotomy₂`, `zero_eq_ofReal`	83
Total	86

ENNReal

Definitions

Name	Category	Theorems
`toNNRealHom` 📖	CompOp	—
`toRealHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_lt_ofReal` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofNNReal` `ofReal` `Real` `Real.instLT` `NNReal.toReal`	—	—
`dichotomy` 📖	mathematical	—	`Top.top` `ENNReal` `instTopENNReal` `Real` `Real.instLE` `Real.instOne` `toReal`	—	`NeZero.charZero_one` `instCharZero` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `trichotomy₂` `Fact.out`
`le_ofReal_iff_toReal_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `toReal`	—	`CanLift.prf` `canLift` `Real.le_toNNReal_iff_coe_le`
`le_toNNReal_of_coe_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofNNReal`	`NNReal` `instPartialOrderNNReal` `toNNReal`	—	`toNNReal_mono` `toNNReal_coe`
`lt_ofReal_iff_toReal_lt` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `Real` `Real.instLT` `toReal`	—	`CanLift.prf` `canLift` `Real.lt_toNNReal_iff_coe_lt`
`natCast_le_ofReal` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ofReal` `Real` `Real.instLE` `Real.instNatCast`	—	`ofReal_lt_natCast`
`natCast_lt_ofReal` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ofReal` `Real` `Real.instLT` `Real.instNatCast`	—	`coe_lt_coe` `Real.natCast_lt_toNNReal`
`ofNat_le_ofReal` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast`	—	`natCast_le_ofReal` `Nat.AtLeastTwo.toNeZero`
`ofNat_lt_ofReal` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `Real` `Real.instLT` `instOfNatAtLeastTwo` `Real.instNatCast`	—	`natCast_lt_ofReal`
`ofReal_add` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ofReal` `Real.instAdd` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`ofReal.eq_1` `coe_add` `Real.toNNReal_add`
`ofReal_add_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `Real` `Real.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`coe_le_coe` `Real.toNNReal_add_le`
`ofReal_eq_natCast` 📖	mathematical	—	`ofReal` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Real` `Real.instNatCast`	—	`Real.toNNReal_eq_natCast`
`ofReal_eq_ofNat` 📖	mathematical	—	`ofReal` `Real` `instOfNatAtLeastTwo` `Real.instNatCast`	—	`ofReal_eq_natCast` `Nat.AtLeastTwo.toNeZero`
`ofReal_eq_ofReal_iff` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ofReal`	—	`ofReal.eq_1` `Real.toNNReal_eq_toNNReal_iff`
`ofReal_eq_one` 📖	mathematical	—	`ofReal` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Real` `Real.instOne`	—	`Real.toNNReal_eq_one`
`ofReal_eq_zero` 📖	mathematical	—	`ofReal` `ENNReal` `instZeroENNReal` `Real` `Real.instLE` `Real.instZero`	—	—
`ofReal_le_coe` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `ofNNReal` `Real` `Real.instLE` `NNReal.toReal`	—	`ofReal_zero` `ofReal_coe_nnreal` `instCanonicallyOrderedAdd`
`ofReal_le_iff_le_toReal` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `Real` `Real.instLE` `toReal`	—	`CanLift.prf` `canLift` `Real.toNNReal_le_iff_le_coe`
`ofReal_le_natCast` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Real` `Real.instLE` `Real.instNatCast`	—	`coe_le_coe` `Real.toNNReal_le_natCast`
`ofReal_le_ofNat` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast`	—	`ofReal_le_natCast`
`ofReal_le_ofReal` 📖	mathematical	`Real` `Real.instLE`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal`	—	`Real.toNNReal_le_toNNReal`
`ofReal_le_ofReal_iff` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal`	—	`ofReal.eq_1` `coe_le_coe` `Real.toNNReal_le_toNNReal_iff`
`ofReal_le_ofReal_iff'` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `Real` `Real.instLE` `Real.instZero`	—	`coe_le_coe` `Real.toNNReal_le_toNNReal_iff'`
`ofReal_le_of_le_toReal` 📖	mathematical	`Real` `Real.instLE` `toReal`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal`	—	`LE.le.trans` `ofReal_le_ofReal` `ofReal_toReal_le`
`ofReal_le_one` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Real` `Real.instLE` `Real.instOne`	—	`coe_le_coe` `Real.toNNReal_le_one`
`ofReal_lt_coe_iff` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `ofNNReal` `Real.instLT` `NNReal.toReal`	—	`ofReal_lt_iff_lt_toReal` `coe_ne_top` `coe_toReal`
`ofReal_lt_iff_lt_toReal` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `Real.instLT` `toReal`	—	`CanLift.prf` `canLift` `Real.toNNReal_lt_iff_lt_coe`
`ofReal_lt_natCast` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Real` `Real.instLT` `Real.instNatCast`	—	`ofReal_natCast` `ofReal_lt_ofReal_iff` `Nat.cast_pos` `Real.instIsOrderedRing` `Real.instNontrivial` `Ne.bot_lt`
`ofReal_lt_ofNat` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `Real` `Real.instLT` `instOfNatAtLeastTwo` `Real.instNatCast`	—	`ofReal_lt_natCast` `Nat.AtLeastTwo.toNeZero`
`ofReal_lt_ofReal_iff` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofReal`	—	`ofReal.eq_1` `coe_lt_coe` `Real.toNNReal_lt_toNNReal_iff`
`ofReal_lt_ofReal_iff'` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `Real` `Real.instLT` `Real.instZero`	—	`coe_lt_coe` `Real.toNNReal_lt_toNNReal_iff'`
`ofReal_lt_ofReal_iff_of_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `Real.instLT`	—	`ofReal.eq_1` `coe_lt_coe` `Real.toNNReal_lt_toNNReal_iff_of_nonneg`
`ofReal_lt_one` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Real` `Real.instLT` `Real.instOne`	—	`Nat.cast_one` `ofReal_lt_natCast` `one_ne_zero`
`ofReal_max` 📖	mathematical	—	`ofReal` `Real` `Real.instMax` `ENNReal` `instMax`	—	`Monotone.map_max` `ofReal_mono`
`ofReal_min` 📖	mathematical	—	`ofReal` `Real` `Real.instMin` `ENNReal` `instMin`	—	`Monotone.map_min` `ofReal_mono`
`ofReal_mono` 📖	mathematical	—	`Monotone` `Real` `ENNReal` `Real.instPreorder` `PartialOrder.toPreorder` `instPartialOrder` `ofReal`	—	`ofReal_le_ofReal`
`ofReal_mul` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ofReal` `Real.instMul` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`Real.toNNReal_mul`
`ofReal_mul'` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ofReal` `Real.instMul` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`mul_comm` `ofReal_mul`
`ofReal_ne_zero_iff` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero`	—	`pos_iff_ne_zero` `instCanonicallyOrderedAdd` `ofReal_pos`
`ofReal_nsmul` 📖	mathematical	—	`ofReal` `Real` `AddMonoid.toNatSMul` `Real.instAddMonoid` `ENNReal` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`nsmul_eq_mul` `ofReal_natCast` `ofReal_mul` `Nat.cast_nonneg` `Real.instIsOrderedRing`
`ofReal_of_nonpos` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ofReal` `ENNReal` `instZeroENNReal`	—	`ofReal_eq_zero`
`ofReal_pos` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `instZeroENNReal` `ofReal` `Real` `Real.instLT` `Real.instZero`	—	—
`ofReal_pow` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ofReal` `Monoid.toNatPow` `Real.instMonoid` `ENNReal` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiring`	—	`ofReal_eq_coe_nnreal` `coe_pow` `ofReal_coe_nnreal` `NNReal.coe_pow`
`one_le_ofReal` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ofReal` `Real` `Real.instLE` `Real.instOne`	—	`Nat.cast_one` `natCast_le_ofReal` `one_ne_zero`
`one_lt_ofReal` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ofReal` `Real` `Real.instLT` `Real.instOne`	—	`coe_lt_coe` `Real.one_lt_toNNReal`
`sup_eq_zero` 📖	mathematical	—	`ENNReal` `instMax` `instZeroENNReal`	—	`sup_eq_bot_iff`
`toNNReal_le_toNNReal` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `toNNReal` `ENNReal` `instPartialOrder`	—	`coe_toNNReal` `coe_le_coe` `toNNReal_mono`
`toNNReal_lt_of_lt_coe` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofNNReal`	`NNReal` `instPartialOrderNNReal` `toNNReal`	—	`toNNReal_strict_mono` `coe_ne_top` `toNNReal_coe`
`toNNReal_lt_toNNReal` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `toNNReal` `ENNReal` `instPartialOrder`	—	`coe_toNNReal` `coe_lt_coe` `toNNReal_strict_mono`
`toNNReal_mono` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`NNReal` `instPartialOrderNNReal` `toNNReal`	—	`toReal_mono`
`toNNReal_mul` 📖	mathematical	—	`toNNReal` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `NNReal` `instSemiringNNReal`	—	`WithTop.untopD_zero_mul`
`toNNReal_mul_top` 📖	mathematical	—	`toNNReal` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Top.top` `instTopENNReal` `NNReal` `instZeroNNReal`	—	`toNNReal_mul` `MulZeroClass.mul_zero`
`toNNReal_pos` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `toNNReal`	—	`toNNReal_pos_iff` `bot_lt_iff_ne_bot` `lt_top_iff_ne_top`
`toNNReal_pos_iff` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `toNNReal` `ENNReal` `instPartialOrder` `instZeroENNReal` `Top.top` `instTopENNReal`	—	—
`toNNReal_pow` 📖	mathematical	—	`toNNReal` `ENNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiring` `NNReal` `instSemiringNNReal`	—	`MonoidHom.map_pow`
`toNNReal_strict_mono` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	`NNReal` `instPartialOrderNNReal` `toNNReal`	—	`coe_toNNReal` `LT.lt.ne_top`
`toNNReal_top_mul` 📖	mathematical	—	`toNNReal` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Top.top` `instTopENNReal` `NNReal` `instZeroNNReal`	—	`toNNReal_mul` `MulZeroClass.zero_mul`
`toReal_add` 📖	mathematical	—	`toReal` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Real` `Real.instAdd`	—	`CanLift.prf` `canLift`
`toReal_add_le` 📖	mathematical	—	`Real` `Real.instLE` `toReal` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Real.instAdd`	—	`top_add` `zero_add` `add_top` `add_zero` `le_of_eq` `toReal_add`
`toReal_eq_toReal` 📖	mathematical	—	`toReal`	—	`toReal_eq_toReal_iff'`
`toReal_inf` 📖	mathematical	—	`toReal` `ENNReal` `instMin` `Real` `Real.instMin`	—	`toReal_min`
`toReal_le_of_le_ofReal` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ofReal`	`toReal`	—	`ne_top_of_le_ne_top` `ofReal_ne_top` `le_ofReal_iff_toReal_le`
`toReal_le_toReal` 📖	mathematical	—	`Real` `Real.instLE` `toReal` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`CanLift.prf` `canLift`
`toReal_lt_of_lt_ofReal` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofReal`	`Real` `Real.instLT` `toReal`	—	`lt_ofReal_iff_toReal_lt` `LT.lt.ne_top`
`toReal_lt_toReal` 📖	mathematical	—	`Real` `Real.instLT` `toReal` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	—	`CanLift.prf` `canLift`
`toReal_max` 📖	mathematical	—	`toReal` `ENNReal` `instMax` `Real` `Real.instMax`	—	`le_total` `max_eq_right` `toReal_mono` `max_eq_left`
`toReal_min` 📖	mathematical	—	`toReal` `ENNReal` `instMin` `Real` `Real.instMin`	—	`le_total` `min_eq_left` `toReal_mono` `min_eq_right`
`toReal_mono` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Real` `Real.instLE` `toReal`	—	`toReal_le_toReal` `ne_top_of_le_ne_top`
`toReal_mono'` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Top.top` `instTopENNReal`	`Real` `Real.instLE` `toReal`	—	`eq_or_ne` `toReal_nonneg` `toReal_mono`
`toReal_mul` 📖	mathematical	—	`toReal` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Real` `Real.instMul`	—	`MonoidWithZeroHom.map_mul`
`toReal_mul_top` 📖	mathematical	—	`toReal` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Top.top` `instTopENNReal` `Real` `Real.instZero`	—	`toReal_mul` `toReal_top` `MulZeroClass.mul_zero`
`toReal_nsmul` 📖	mathematical	—	`toReal` `ENNReal` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Real` `Real.instAddMonoid`	—	`nsmul_eq_mul` `toReal_mul` `toReal_natCast`
`toReal_ofReal_mul` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`toReal` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `ofReal` `Real.instMul`	—	`toReal_mul` `toReal_ofReal`
`toReal_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `toReal`	—	`toReal_pos_iff` `bot_lt_iff_ne_bot` `lt_top_iff_ne_top`
`toReal_pos_iff` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `toReal` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `instZeroENNReal` `Top.top` `instTopENNReal`	—	`NNReal.coe_pos` `toNNReal_pos_iff`
`toReal_pos_iff_ne_top` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `toReal`	—	`LT.lt.ne` `toReal_top` `LT.lt.trans_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `dichotomy`
`toReal_pow` 📖	mathematical	—	`toReal` `ENNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiring` `Real` `Real.instMonoid`	—	`MonoidHom.map_pow`
`toReal_strict_mono` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	`Real` `Real.instLT` `toReal`	—	`toReal_lt_toReal` `LT.lt.ne_top`
`toReal_sup` 📖	mathematical	—	`toReal` `ENNReal` `instMax` `Real` `Real.instMax`	—	`toReal_max`
`toReal_top_mul` 📖	mathematical	—	`toReal` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Top.top` `instTopENNReal` `Real` `Real.instZero`	—	`mul_comm` `toReal_mul_top`
`trichotomy` 📖	mathematical	—	`ENNReal` `instZeroENNReal` `Top.top` `instTopENNReal` `Real` `Real.instLT` `Real.instZero` `toReal`	—	`toReal_pos`
`trichotomy₂` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instZeroENNReal` `Top.top` `instTopENNReal` `Real` `Real.instLT` `Real.instZero` `toReal` `Real.instLE`	—	`eq_or_lt_of_le` `bot_le` `trichotomy` `le_top` `lt_of_lt_of_le` `lt_of_le_of_lt` `toReal_mono` `LT.lt.ne`
`zero_eq_ofReal` 📖	mathematical	—	`ENNReal` `instZeroENNReal` `ofReal` `Real` `Real.instLE` `Real.instZero`	—	`ofReal_eq_zero`

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalENNRealOfReal` 📖	CompOp	—

---

← Back to Index