minCardFinsetOfMemConvexHull_nonempty

English

The min-cardinal finite hull is affinely independent.

Русский

Минимальная по размеру выпуклая оболочка является аффинно независимой.

LaTeX

$$$\\operatorname{AffineIndependent}(\\text{minCardFinsetOfMemConvexHull}(x))$$$

Lean4

theorem minCardFinsetOfMemConvexHull_nonempty : (minCardFinsetOfMemConvexHull hx).Nonempty :=
  by
  rw [← Finset.coe_nonempty, ← @convexHull_nonempty_iff 𝕜]
  exact ⟨x, mem_minCardFinsetOfMemConvexHull hx⟩

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