chainHeight_eq_zero_iff

Mathlib.Order.Height

URI: https://scilib.ai/kg/mathlib#Set.chainHeight_eq_zero_iff

← MathLib Explorer

English

s.chainHeight = 0 if and only if s is empty.

Русский

s.chainHeight = 0 эквивалентно тому, что s пусто.

LaTeX

$$$ s.chainHeight = 0 \\iff s = \\emptyset. $$$

Lean4

@[simp]
theorem chainHeight_eq_zero_iff : s.chainHeight = 0 ↔ s = ∅ := by
  rw [← not_iff_not, ← Ne, ← ENat.one_le_iff_ne_zero, one_le_chainHeight_iff, nonempty_iff_ne_empty]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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