card_le_of_finset

Mathlib.SetTheory.Cardinal.Order

URI: https://scilib.ai/kg/mathlib#Cardinal.card_le_of_finset

English

The cardinality of a Finset s is at most the cardinality of the ambient type α.

Русский

Кардинал множества Finset s не превосходит кардинал множества α.

LaTeX

$$$(\mathrm{card}(s) : \mathrm{Cardinal}) \le \#\alpha$$$

Lean4

theorem card_le_of_finset {α} (s : Finset α) : (s.card : Cardinal) ≤ #α :=
  @mk_coe_finset _ s ▸ mk_set_le _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru