English
A convex set is strictly convex provided that for any distinct x,y in s\Int(s), the line segment joining x and y meets Int(s).
Русский
Выпуклое множество строго выпукло в смысле, что любые две разные точки вне interior(s) соединяемой отрезок пересекает interior(s).
LaTeX
$$$$\text{StrictConvex}'(s)\;:\; (s\setminus\operatorname{Int}(s))\text{ pairs with lineMap intersects interior of } s.$$$$
Lean4
/-- A convex set `s` is strictly convex provided that for any two distinct points of
`s \ interior s`, the line passing through these points has nonempty intersection with
`interior s`. -/
protected theorem strictConvex' {s : Set E} (hs : Convex 𝕜 s)
(h : (s \ interior s).Pairwise fun x y => ∃ c : 𝕜, lineMap x y c ∈ interior s) : StrictConvex 𝕜 s :=
by
refine strictConvex_iff_openSegment_subset.2 ?_
intro x hx y hy hne
by_cases hx' : x ∈ interior s
· exact hs.openSegment_interior_self_subset_interior hx' hy
by_cases hy' : y ∈ interior s
· exact hs.openSegment_self_interior_subset_interior hx hy'
rcases h ⟨hx, hx'⟩ ⟨hy, hy'⟩ hne with ⟨c, hc⟩
refine (openSegment_subset_union x y ⟨c, rfl⟩).trans (insert_subset_iff.2 ⟨hc, union_subset ?_ ?_⟩)
exacts [hs.openSegment_self_interior_subset_interior hx hc, hs.openSegment_interior_self_subset_interior hc hy]
