English
As above: the min-cardinal finite hull is affinely independent.
Русский
Как выше: минимальное по размеру конечное множество выпуклой оболочки аффинно независимо.
LaTeX
$$$\\text{AffineIndependent}(\\text{minCardFinsetOfMemConvexHull}(x))$$$
Lean4
theorem affineIndependent_minCardFinsetOfMemConvexHull :
AffineIndependent 𝕜 ((↑) : minCardFinsetOfMemConvexHull hx → E) :=
by
let k := #(minCardFinsetOfMemConvexHull hx) - 1
have hk : #(minCardFinsetOfMemConvexHull hx) = k + 1 :=
(Nat.succ_pred_eq_of_pos (Finset.card_pos.mpr (minCardFinsetOfMemConvexHull_nonempty hx))).symm
classical
by_contra h
obtain ⟨p, hp⟩ := mem_convexHull_erase h (mem_minCardFinsetOfMemConvexHull hx)
have contra :=
minCardFinsetOfMemConvexHull_card_le_card hx
(Set.Subset.trans (Finset.erase_subset (p : E) (minCardFinsetOfMemConvexHull hx))
(minCardFinsetOfMemConvexHull_subseteq hx))
hp
rw [← not_lt] at contra
apply contra
rw [card_erase_of_mem p.2, hk]
exact lt_add_one _
