card_eq_zero

Mathlib.SetTheory.Cardinal.Finite

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

English

Nat.card α = 0 if and only if α is empty or infinite.

Русский

Nat.card α = 0 тогда и только тогда, когда α пусто или бесконечно.

LaTeX

$$$ \mathrm{Nat.card}\alpha = 0 \iff \mathrm{IsEmpty}\alpha \lor \mathrm{Infinite}\alpha $$$

Lean4

theorem card_eq_zero : Nat.card α = 0 ↔ IsEmpty α ∨ Infinite α := by simp [Nat.card, mk_eq_zero_iff, aleph0_le_mk_iff]

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

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

Разделы

Аффилиация

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