convexHull_subset_iff — Mathlib

English

If t is convex, then convexHull 𝕜 s is contained in t if and only if s is contained in t.

Русский

Если t выпукло, то выпуклая оболочка s содержится в t тогда и только тогда, когда s содержится в t.

LaTeX

$$$ (ht : Convex 𝕜 t) : convexHull 𝕜 s \\subseteq t \\iff s \\subseteq t $$$

Lean4

theorem convexHull_subset_iff (ht : Convex 𝕜 t) : convexHull 𝕜 s ⊆ t ↔ s ⊆ t :=
  (show (convexHull 𝕜).IsClosed t from ht).closure_le_iff

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