strictConvex — Mathlib

English

If a set is OrdConnected, then it is strictly convex.

Русский

Если множество OrdConnected, то оно строго выпукло.

LaTeX

$$$(s : Set \beta) \; (hs : OrdConnected s) : StrictConvex 𝕜 s$$$

Lean4

protected theorem strictConvex {s : Set β} (hs : OrdConnected s) : StrictConvex 𝕜 s :=
  by
  refine strictConvex_iff_openSegment_subset.2 fun x hx y hy hxy => ?_
  rcases hxy.lt_or_gt with hlt | hlt <;> [skip; rw [openSegment_symm]] <;>
    exact
      (openSegment_subset_Ioo hlt).trans
        (isOpen_Ioo.subset_interior_iff.2 <| Ioo_subset_Icc_self.trans <| hs.out ‹_› ‹_›)

Похожие утверждения