convexHull_inter_convexHull — Mathlib

English

For faces s,t of K, the intersection of their convex hulls equals the convex hull of their intersection.

Русский

Для граней s,t K пересечение выпуклых оболочек равно выпуклой оболочке пересечения s и t.

LaTeX

$$$\\text{convexHull } 𝕜 ↑s \\cap \\text{convexHull } 𝕜 ↑t = \\text{convexHull } 𝕜 (s \\cap t : Set E)$$$

Lean4

theorem convexHull_inter_convexHull (hs : s ∈ K.faces) (ht : t ∈ K.faces) :
    convexHull 𝕜 ↑s ∩ convexHull 𝕜 ↑t = convexHull 𝕜 (s ∩ t : Set E) :=
  (K.inter_subset_convexHull hs ht).antisymm <|
    subset_inter (convexHull_mono Set.inter_subset_left) <| convexHull_mono Set.inter_subset_right

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