Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-11 07:59 9709d60a

View on Github →

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.

Estimated changes

modified theorem strict_convex_Icc
modified theorem strict_convex_Ici
modified theorem strict_convex_Ico
modified theorem strict_convex_Iic
modified theorem strict_convex_Iio
modified theorem strict_convex_Ioc
modified theorem strict_convex_Ioi
modified theorem strict_convex_Ioo
modified theorem strict_convex_iff_convex
modified theorem strict_convex_interval