face_subset_face_iff — Mathlib

English

For faces s and t that are faces of K, convexHull(s) ⊆ convexHull(t) if and only if s ⊆ t.

Русский

Для граней s и t комплексa K выполнено: выпуклая оболочка s содержится в выпуклой оболочке t тогда и только тогда, когда s ⊆ t.

LaTeX

$$$(hs \\in K.faces) (ht \\in K.faces) \\Rightarrow (convexHull 𝕜 (s : Set E) \\subseteq convexHull 𝕜 ↑t \\iff s \\subseteq t)$$$

Lean4

/-- A face is a subset of another one iff its vertices are. -/
theorem face_subset_face_iff (hs : s ∈ K.faces) (ht : t ∈ K.faces) :
    convexHull 𝕜 (s : Set E) ⊆ convexHull 𝕜 ↑t ↔ s ⊆ t :=
  ⟨fun h _ hxs =>
    (vertex_mem_convexHull_iff (K.down_closed hs (Finset.singleton_subset_iff.2 hxs) <| singleton_ne_empty _) ht).1
      (h (subset_convexHull 𝕜 (E := E) s hxs)),
    convexHull_mono⟩

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