set_fintype_card_le_univ — Mathlib

English

Let α be a finite type and s ⊆ α be any subset which is itself finite. Then the number of elements in s does not exceed the number of elements in α; i.e., |s| ≤ |α|.

Русский

Пусть α конечного типа и s ⊆ α — произвольное подмножество, которое также конечное. Тогда кардинальность s не превосходит кардинальность α; то есть |s| ≤ |α|.

LaTeX

$$$|s| \le |\alpha|$$$

Lean4

theorem set_fintype_card_le_univ [Fintype α] (s : Set α) [Fintype s] : Fintype.card s ≤ Fintype.card α :=
  Fintype.card_le_of_embedding (Function.Embedding.subtype s)

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