isOrdinal_empty

Mathlib.SetTheory.ZFC.Ordinal

URI: https://scilib.ai/kg/mathlib#ZFSet.isOrdinal_empty

English

The empty set is an ordinal.

Русский

Пустое множество является ординалом.

LaTeX

$$$IsOrdinal(\varnothing)$$$

Lean4

@[simp]
theorem isOrdinal_empty : IsOrdinal ∅ :=
  ⟨isTransitive_empty, fun _ _ H ↦ (notMem_empty _ H).elim⟩

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

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

Разделы

Аффилиация

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