vertex_mem_convexHull_iff — Mathlib

English

If x is a vertex and s is a face, then x lies in the convex hull of s if and only if x ∈ s.

Русский

Если x — вершина, а s — грань, то x лежит в выпуклой оболочке s тогда и только тогда, когда x ∈ s.

LaTeX

$$$(x \\in K.vertices) \\land (s \\in K.faces) \\Rightarrow (x \\in convexHull 𝕜 (s : Set E) \\iff x \\in s)$$$

Lean4

theorem vertex_mem_convexHull_iff (hx : x ∈ K.vertices) (hs : s ∈ K.faces) : x ∈ convexHull 𝕜 (s : Set E) ↔ x ∈ s :=
  by
  refine ⟨fun h => ?_, fun h => subset_convexHull 𝕜 _ h⟩
  classical
  have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
  by_contra H
  rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm, coe_empty,
    convexHull_empty] at h

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