length_le_card — Mathlib

English

If l is a nodup list of elements of α, then length(l) ≤ card(α).

Русский

Если список l без повторов элементов α, то длина списка не превосходит кардинала α.

LaTeX

$$$ \mathrm{length}(l) \le |\alpha| $$$

Lean4

theorem length_le_card {α : Type*} [Fintype α] {l : List α} (h : l.Nodup) : l.length ≤ Fintype.card α := by
  classical exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ

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