card_eq_zero_of_infinite

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#Nat.card_eq_zero_of_infinite

English

If α is infinite, then Nat.card α = 0.

Русский

Если множество α бесконечно, то Nat.card α = 0.

LaTeX

$$$ [\mathrm{Infinite}\,\alpha] \rightarrow \mathrm{Nat.card}\alpha = 0 $$$

Lean4

@[simp]
theorem card_eq_zero_of_infinite [Infinite α] : Nat.card α = 0 :=
  mk_toNat_of_infinite

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

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

Разделы

Аффилиация

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