segment_subset_convexJoin — Mathlib

English

For x in s and y in t, the segment from x to y is contained in convexJoin 𝕜 s t.

Русский

Для x ∈ s и y ∈ t остаток отрезка x y принадлежит convexJoin 𝕜 s t.

LaTeX

$$$ (x \in s) \land (y \in t) \Rightarrow segment 𝕜 x y \subseteq convexJoin 𝕜 s t $$$

Lean4

theorem segment_subset_convexJoin (hx : x ∈ s) (hy : y ∈ t) : segment 𝕜 x y ⊆ convexJoin 𝕜 s t :=
  subset_iUnion₂_of_subset x hx <| subset_iUnion₂ (s := fun y _ ↦ segment 𝕜 x y) y hy

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