minCardFinsetOfMemConvexHull_card_le_card

English

The cardinality of the min-card finite subset is at most the cardinality of t.

Русский

Кардинальность минимального по объёму конечного подмножества не превосходит кардинальности исходного множества t.

LaTeX

$$$\\#(\\text{minCardFinsetOfMemConvexHull}(x))\\leq \\#t$$$

Lean4

theorem minCardFinsetOfMemConvexHull_card_le_card {t : Finset E} (ht₁ : ↑t ⊆ s) (ht₂ : x ∈ convexHull 𝕜 (t : Set E)) :
    #(minCardFinsetOfMemConvexHull hx) ≤ #t :=
  Function.argminOn_le _ _ (by exact ⟨ht₁, ht₂⟩)

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