card_ne_zero

Mathlib.SetTheory.Cardinal.Finite

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

English

Nat.card α ≠ 0 if and only if α is nonempty and finite.

Русский

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

LaTeX

$$$ \mathrm{Nat.card}\alpha \neq 0 \iff \mathrm{Nonempty}\alpha \land \mathrm{Finite}\alpha $$$

Lean4

theorem card_ne_zero : Nat.card α ≠ 0 ↔ Nonempty α ∧ Finite α := by simp [card_eq_zero, not_or]

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

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

Разделы

Аффилиация

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