segment_subset_convexHull — Mathlib

English

If x,y are in s, then the line segment between x and y is contained in the convex hull of s.

Русский

Если x,y принадлежат s, то отрезок между x и y лежит внутри выпуклой оболочки s.

LaTeX

$$$ x \\in s \\to y \\in s \\to segment 𝕜 x y \\subseteq convexHull 𝕜 s $$$

Lean4

theorem segment_subset_convexHull (hx : x ∈ s) (hy : y ∈ s) : segment 𝕜 x y ⊆ convexHull 𝕜 s :=
  (convex_convexHull _ _).segment_subset (subset_convexHull _ _ hx) (subset_convexHull _ _ hy)

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