Commit 2022-01-24 16:03 155c3309

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.