English
A convex set is strictly convex if for any two distinct points in s\Int(s), the segment between them has a point in Int(s).
Русский
Выпуклoе множество строго выпукло, если для любых двух различных точек в s\Int(s) отрезок между ними имеет точку в Int(s).
LaTeX
$$$$\text{StrictConvex}(s)\;:\; (s\setminus\operatorname{Int}(s))\text{ pairs with nonempty intersection with } \operatorname{Int}(s).$$$$
Lean4
/-- A convex set `s` is strictly convex provided that for any two distinct points `x`, `y` of
`s \ interior s`, the segment with endpoints `x`, `y` has nonempty intersection with
`interior s`. -/
protected theorem strictConvex {s : Set E} (hs : Convex 𝕜 s)
(h : (s \ interior s).Pairwise fun x y => ([x -[𝕜] y] \ frontier s).Nonempty) : StrictConvex 𝕜 s :=
by
refine hs.strictConvex' <| h.imp_on fun x hx y hy _ => ?_
simp only [segment_eq_image_lineMap, ← self_diff_frontier]
rintro ⟨_, ⟨⟨c, hc, rfl⟩, hcs⟩⟩
refine ⟨c, hs.segment_subset hx.1 hy.1 ?_, hcs⟩
exact (segment_eq_image_lineMap 𝕜 x y).symm ▸ mem_image_of_mem _ hc
