convexHull_pair — Mathlib

English

The convex hull of the union of convexHull s with t equals the convex hull of the union of s with t.

Русский

Выпуклая оболочка объединения выпуклой оболочки s с t равна выпуклой оболочке объединения s с t.

LaTeX

$$$ convexHull 𝕜 (convexHull 𝕜 s \\cup t) = convexHull 𝕜 (s \\cup t) $$$

Lean4

@[simp]
theorem convexHull_pair [IsOrderedRing 𝕜] (x y : E) : convexHull 𝕜 { x, y } = segment 𝕜 x y :=
  by
  refine
    (convexHull_min ?_ <| convex_segment _ _).antisymm
      (segment_subset_convexHull (mem_insert _ _) <| subset_insert _ _ <| mem_singleton _)
  rw [insert_subset_iff, singleton_subset_iff]
  exact ⟨left_mem_segment _ _ _, right_mem_segment _ _ _⟩

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