convexJoin_singleton_segment — Mathlib

English

Symmetric statement to the previous one: convexJoin({a}, segment(b,c)) = convHull{a,b,c}.

Русский

Симметричное утверждение: convexJoin{a}, segment(b,c) = convHull{a,b,c}.

LaTeX

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

Lean4

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

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