convexJoin_segment_singleton — Mathlib

English

The join of a segment with a singleton is the convex hull of the two endpoints and the singleton: convexJoin(seg(a,b), {c}) = convHull{a,b,c}.

Русский

Объединение отрезка и единичного множества даёт выпуклую оболочку трёх точек: convexJoin(seg(a,b), {c}) = convHull{a,b,c}.

LaTeX

$$$\\operatorname{convexJoin}_{\\mathbb{K}}(\\operatorname{segment}_{\\mathbb{K}}(a,b),\\{c\\})=\\operatorname{convexHull}_{\\mathbb{K}}\\{a,b,c\\}. $$$

Lean4

theorem convexJoin_segment_singleton (a b c : E) : convexJoin 𝕜 (segment 𝕜 a b) { c } = convexHull 𝕜 { a, b, c } := by
  rw [← pair_eq_singleton, ← convexJoin_segments, segment_same, pair_eq_singleton]

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