card_pos_iff

Mathlib.SetTheory.Cardinal.Finite

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

English

0 < Nat.card α iff α is nonempty and finite.

Русский

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

LaTeX

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

Lean4

theorem card_pos_iff : 0 < Nat.card α ↔ Nonempty α ∧ Finite α := by simp [Nat.card, mk_eq_zero_iff, mk_lt_aleph0_iff]

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

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

Разделы

Аффилиация

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