Specific lemmas about convexity over ℝ≥0

This file collects some specific results about convexity over the ring ℝ≥0. Expand as needed.

theorem NNReal.Icc_subset_segment {x y : NNReal} : Set.Icc x y ⊆ segment NNReal x y

theorem NNReal.segment_eq_Icc {x y : NNReal} (hxy : x ≤ y) : segment NNReal x y = Set.Icc x y

theorem NNReal.segment_eq_uIcc {x y : NNReal} : segment NNReal x y = Set.uIcc x y

theorem NNReal.convex_iff {M : Type u_1} [AddCommMonoid M] [Module ℝ M] {s : Set M} : Convex NNReal s ↔ Convex ℝ s