NNReal

📁 Source: Mathlib/Analysis/Convex/NNReal.lean

Statistics

Metric	Count
Definitions	0
Theorems Icc_subset_segment, convex_iff, segment_eq_Icc, segment_eq_uIcc	4
Total	4

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_subset_segment 📖	mathematical	—	Set NNReal Set.instHasSubset Set.Icc PartialOrder.toPreorder instPartialOrderNNReal segment instSemiringNNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring Algebra.id	—	Nonneg.Icc_subset_segment Real.instIsStrictOrderedRing
convex_iff 📖	mathematical	—	Convex NNReal instSemiringNNReal instPartialOrderNNReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instDistribMulActionOfReal Module.toDistribMulAction Real Real.semiring Real.partialOrder Real.instMonoid	—	zero_le instCanonicallyOrderedAdd eq Convex.lift Real.instZeroLEOneClass instIsScalarTowerOfReal IsScalarTower.left IsOrderedModule.toSMulPosMono IsStrictOrderedModule.toIsOrderedModule instIsStrictOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing
segment_eq_Icc 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	segment instSemiringNNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring Algebra.id Set.Icc	—	Nonneg.segment_eq_Icc Real.instIsStrictOrderedRing
segment_eq_uIcc 📖	mathematical	—	segment NNReal instSemiringNNReal instPartialOrderNNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring Algebra.id Set.uIcc ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Nonneg.segment_eq_uIcc Real.instIsStrictOrderedRing

---

← Back to Index