isTransitive_empty

Mathlib.SetTheory.ZFC.Ordinal

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

English

The empty set is transitive: IsTransitive ∅.

Русский

Пустое множество транзитивно: IsTransitive ∅.

LaTeX

$$$ \\text{IsTransitive}(\\emptyset). $$$

Lean4

@[simp]
theorem isTransitive_empty : IsTransitive ∅ := fun y hy => (notMem_empty y hy).elim

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

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

Разделы

Аффилиация

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