affineSpan_convexHull — Mathlib

English

The affine span of the convex hull of s equals the affine span of s.

Русский

Аффинное пространство оболочки выпуклого оболочки от s равно аффинному пространству от s.

LaTeX

$$$ affineSpan 𝕜 (convexHull 𝕜 s) = affineSpan 𝕜 s $$$

Lean4

@[simp]
theorem affineSpan_convexHull (s : Set E) : affineSpan 𝕜 (convexHull 𝕜 s) = affineSpan 𝕜 s :=
  by
  refine le_antisymm ?_ (affineSpan_mono 𝕜 (subset_convexHull 𝕜 s))
  rw [affineSpan_le]
  exact convexHull_subset_affineSpan s

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