card_finset_fin_le — Mathlib

English

Let n be a natural number and s be a Finset of Fin(n). Then the cardinality of s satisfies |s| ≤ n.

Русский

Пусть n — натуральное число и s — конечное множество элементов Fin(n). Тогда |s| ≤ n.

LaTeX

$$$$ \forall {n : \mathbb{N}} \ (s : \mathrm{Finset}(\mathrm{Fin}(n))), \#s \le n $$$$

Lean4

theorem card_finset_fin_le {n : ℕ} (s : Finset (Fin n)) : #s ≤ n := by
  simpa only [Fintype.card_fin] using s.card_le_univ

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