mathlib

9709d60a - refactor(analysis/convex/strict): rename, golf, generalize (#17464)

refactor(analysis/convex/strict): rename, golf, generalize (#17464) * rename `convex.strict_convex` to `convex.strict_convex_of_open`; * prove `set.ord_connected.strict_convex`; * use it to prove `strict_convex_Ixx` and golf `strict_convex_iff_convex`.