Basic

📁 Source: Mathlib/Data/NNReal/Basic.lean

Statistics

Metric	Count
Definitions `instFloorSemiring`	1
Theorems `bddAbove_natCast_image_iff`, `bddAbove_range_natCast_iff`, `coe_expect`, `coe_indicator`, `coe_list_prod`, `coe_list_sum`, `coe_mulIndicator`, `coe_mulSingle`, `coe_multiset_prod`, `coe_multiset_sum`, `coe_prod`, `coe_single`, `coe_sum`, `finset_sup_div`, `finset_sup_mul`, `iInf_mul`, `iSup_div`, `iSup_mul`, `iSup_mul_iSup_le`, `iSup_mul_le`, `image_coe_Icc`, `image_coe_Ici`, `image_coe_Ico`, `image_coe_Iic`, `image_coe_Iio`, `image_coe_Ioc`, `image_coe_Ioi`, `image_coe_Ioo`, `image_coe_uIcc`, `image_coe_uIoc`, `image_coe_uIoo`, `le_iInf_add_iInf`, `le_iInf_mul`, `le_iInf_mul_iInf`, `le_mul_iInf`, `mul_finset_sup`, `mul_iInf`, `mul_iSup`, `mul_iSup_le`, `natCast_iInf`, `natCast_iSup`, `range_coe`, `sub_div`, `toNNReal_prod_of_nonneg`, `toNNReal_sum_of_nonneg`	45
Total	46

NNReal

Definitions

Name	Category	Theorems
`instFloorSemiring` 📖	CompOp	4 math math: `ENat.floor_coe`, `Int.abs_le_floor_nnreal_iff`, `ENat.ceil_coe`, `Polynomial.card_mahlerMeasure_le_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove_natCast_image_iff` 📖	mathematical	—	`BddAbove` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Set.image` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`instCanonicallyOrderedAdd` `addLeftMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing`
`bddAbove_range_natCast_iff` 📖	mathematical	—	`BddAbove` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Set.range` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`bddAbove_natCast_image_iff` `Set.range_comp`
`coe_expect` 📖	mathematical	—	`toReal` `Finset.expect` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Algebra.toModule` `NNRat` `instCommSemiringNNRat` `DivisionSemiring.toNNRatAlgebra` `Semifield.toDivisionSemiring` `instSemifield` `IsStrictOrderedRing.toCharZero` `DivisionSemiring.toSemiring` `instPartialOrderNNReal` `instIsStrictOrderedRing` `Real` `Real.instAddCommMonoid` `Real.semiring` `Field.toSemifield` `Real.instField` `Real.partialOrder` `Real.instIsStrictOrderedRing`	—	`map_expect` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `Real.instIsStrictOrderedRing` `RingHomClass.toLinearMapClassNNRat` `RingHom.instRingHomClass`
`coe_indicator` 📖	mathematical	—	`toReal` `Set.indicator` `NNReal` `instZeroNNReal` `Real` `Real.instZero`	—	`map_indicator` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`coe_list_prod` 📖	mathematical	—	`toReal` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instOneNNReal` `Real` `Real.instMul` `Real.instOne`	—	`map_list_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`coe_list_sum` 📖	mathematical	—	`toReal` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instZeroNNReal` `Real` `Real.instAdd` `Real.instZero`	—	`map_list_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `Real.instIsStrictOrderedRing` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomClass.toLinearMapClassNNRat` `RingHom.instRingHomClass`
`coe_mulIndicator` 📖	mathematical	—	`toReal` `Set.mulIndicator` `NNReal` `instOneNNReal` `Real` `Real.instOne`	—	`map_mulIndicator` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`coe_mulSingle` 📖	mathematical	—	`toReal` `Pi.mulSingle` `NNReal` `instOneNNReal` `Real` `Real.instOne`	—	`Set.mulIndicator_singleton` `coe_mulIndicator`
`coe_multiset_prod` 📖	mathematical	—	`toReal` `Multiset.prod` `NNReal` `CommSemiring.toCommMonoid` `instCommSemiringNNReal` `Real` `Real.instCommMonoid` `Multiset.map`	—	`map_multiset_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`coe_multiset_sum` 📖	mathematical	—	`toReal` `Multiset.sum` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `Real.instAddCommMonoid` `Multiset.map`	—	`map_multiset_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `Real.instIsStrictOrderedRing` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomClass.toLinearMapClassNNRat` `RingHom.instRingHomClass`
`coe_prod` 📖	mathematical	—	`toReal` `Finset.prod` `NNReal` `CommSemiring.toCommMonoid` `instCommSemiringNNReal` `Real` `Real.instCommMonoid`	—	`map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`coe_single` 📖	mathematical	—	`toReal` `Pi.single` `NNReal` `instZeroNNReal` `Real` `Real.instZero`	—	`Set.indicator_singleton` `coe_indicator`
`coe_sum` 📖	mathematical	—	`toReal` `Finset.sum` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `Real.instAddCommMonoid`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `Real.instIsStrictOrderedRing` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomClass.toLinearMapClassNNRat` `RingHom.instRingHomClass`
`finset_sup_div` 📖	mathematical	—	`NNReal` `instDiv` `Finset.sup` `instSemilatticeSupNNReal` `instOrderBot`	—	`div_eq_inv_mul` `mul_finset_sup`
`finset_sup_mul` 📖	mathematical	—	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Finset.sup` `instSemilatticeSupNNReal` `instOrderBot`	—	`Finset.comp_sup_eq_sup_comp` `sup_mul` `MulZeroClass.zero_mul`
`iInf_mul` 📖	mathematical	—	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`coe_mul` `coe_iInf` `Real.iInf_mul_of_nonneg` `coe_nonneg`
`iSup_div` 📖	mathematical	—	`NNReal` `instDiv` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`div_eq_mul_inv` `iSup_mul`
`iSup_mul` 📖	mathematical	—	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`mul_comm` `mul_iSup`
`iSup_mul_iSup_le` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`iSup_mul_le` `mul_iSup_le`
`iSup_mul_le` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`iSup_mul` `ciSup_le'`
`image_coe_Icc` 📖	mathematical	—	`Set.image` `NNReal` `Real` `toReal` `Set.Icc` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Real.instPreorder`	—	`Set.image_subtype_val_Icc` `Set.ordConnected_Ici`
`image_coe_Ici` 📖	mathematical	—	`Set.image` `NNReal` `Real` `toReal` `Set.Ici` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Real.instPreorder`	—	`Set.image_subtype_val_Ici_Ici`
`image_coe_Ico` 📖	mathematical	—	`Set.image` `NNReal` `Real` `toReal` `Set.Ico` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Real.instPreorder`	—	`Set.image_subtype_val_Ico` `Set.ordConnected_Ici`
`image_coe_Iic` 📖	mathematical	—	`Set.image` `NNReal` `Real` `toReal` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Set.Icc` `Real.instPreorder` `Real.instZero`	—	`Set.image_subtype_val_Ici_Iic`
`image_coe_Iio` 📖	mathematical	—	`Set.image` `NNReal` `Real` `toReal` `Set.Iio` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Set.Ico` `Real.instPreorder` `Real.instZero`	—	`Set.image_subtype_val_Ici_Iio`
`image_coe_Ioc` 📖	mathematical	—	`Set.image` `NNReal` `Real` `toReal` `Set.Ioc` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Real.instPreorder`	—	`Set.image_subtype_val_Ioc` `Set.ordConnected_Ici`
`image_coe_Ioi` 📖	mathematical	—	`Set.image` `NNReal` `Real` `toReal` `Set.Ioi` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Real.instPreorder`	—	`Set.image_subtype_val_Ici_Ioi`
`image_coe_Ioo` 📖	mathematical	—	`Set.image` `NNReal` `Real` `toReal` `Set.Ioo` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Real.instPreorder`	—	`Set.image_subtype_val_Ioo` `Set.ordConnected_Ici`
`image_coe_uIcc` 📖	mathematical	—	`Set.image` `NNReal` `Real` `toReal` `Set.uIcc` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Real.lattice`	—	`Set.image_subtype_val_uIcc` `Set.ordConnected_Ici`
`image_coe_uIoc` 📖	mathematical	—	`Set.image` `NNReal` `Real` `toReal` `Set.uIoc` `instLinearOrder` `Real.linearOrder`	—	`Set.image_subtype_val_uIoc` `Set.ordConnected_Ici`
`image_coe_uIoo` 📖	mathematical	—	`Set.image` `NNReal` `Real` `toReal` `Set.uIoo` `instLinearOrder` `Real.linearOrder`	—	`Set.image_subtype_val_uIoo` `Set.ordConnected_Ici`
`le_iInf_add_iInf` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`coe_le_coe` `coe_add` `coe_iInf` `le_ciInf_add_ciInf` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`le_iInf_mul` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`iInf_mul` `le_ciInf`
`le_iInf_mul_iInf` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`le_iInf_mul` `le_mul_iInf`
`le_mul_iInf` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`mul_iInf` `le_ciInf`
`mul_finset_sup` 📖	mathematical	—	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Finset.sup` `instSemilatticeSupNNReal` `instOrderBot`	—	`Finset.comp_sup_eq_sup_comp` `mul_sup` `MulZeroClass.mul_zero`
`mul_iInf` 📖	mathematical	—	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`mul_comm` `iInf_mul`
`mul_iSup` 📖	mathematical	—	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`coe_mul` `coe_iSup` `Real.mul_iSup_of_nonneg` `coe_nonneg`
`mul_iSup_le` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`mul_iSup` `ciSup_le'`
`natCast_iInf` 📖	mathematical	—	`NNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `iInf` `Nat.instInfSet` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`isEmpty_or_nonempty` `Nat.iInf_of_empty` `Nat.cast_zero` `iInf_empty` `eq_of_forall_le_iff`
`natCast_iSup` 📖	mathematical	—	`NNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `iSup` `Nat.instSupSet` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`eq_of_forall_ge_iff` `instCanonicallyOrderedAdd` `ciSup_of_not_bddAbove` `csSup_empty` `Nat.cast_zero` `bot_eq_zero'`
`range_coe` 📖	mathematical	—	`Set.range` `Real` `NNReal` `toReal` `Set.Ici` `Real.instPreorder` `Real.instZero`	—	`Subtype.range_coe`
`sub_div` 📖	mathematical	—	`NNReal` `instDiv` `instSub`	—	`tsub_div` `instCanonicallyOrderedAdd` `instIsStrictOrderedRing` `instOrderedSub`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toNNReal_prod_of_nonneg` 📖	mathematical	`Real` `instLE` `instZero`	`toNNReal` `Finset.prod` `instCommMonoid` `NNReal` `CommSemiring.toCommMonoid` `instCommSemiringNNReal`	—	`NNReal.coe_prod` `coe_toNNReal` `Finset.prod_nonneg` `instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `Finset.prod_congr`
`toNNReal_sum_of_nonneg` 📖	mathematical	`Real` `instLE` `instZero`	`toNNReal` `Finset.sum` `instAddCommMonoid` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`NNReal.coe_sum` `coe_toNNReal` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Finset.sum_congr`

---

← Back to Index