mathlib3

155c3309 - feat(analysis/convex/{basic,function}): add lemmas, golf (#11608)

feat(analysis/convex/{basic,function}): add lemmas, golf (#11608) * add `segment_subset_iff`, `open_segment_subset_iff`, use them to golf some proofs; * add `mem_segment_iff_div`, `mem_open_segment_iff_div`, use the former in the proof of `convex_iff_div`; * move the proof of `mpr` in `convex_on_iff_convex_epigraph` to a new lemma; * prove that the strict epigraph of a convex function include the open segment provided that one of the endpoints is in the strong epigraph and the other is in the epigraph; use it in the proof of `convex_on.convex_strict_epigraph`.