card_of_isEmpty

Mathlib.SetTheory.Cardinal.Finite

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

English

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

Русский

Если множество α пусто, то Nat.card α = 0.

LaTeX

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

Lean4

@[simp]
theorem card_of_isEmpty [IsEmpty α] : Nat.card α = 0 := by simp [Nat.card]

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

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

Разделы

Аффилиация

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