chainHeight_of_isEmpty

Mathlib.Order.Height

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

English

If α is an empty type, then every set s ⊆ α has chainHeight 0.

Русский

Если тип α пуст, то для любого множества s ⊆ α цепная высота равна 0.

LaTeX

$$[IsEmpty α] ⇒ ∀ s : Set α, s.chainHeight = 0$$

Lean4

@[simp]
theorem chainHeight_of_isEmpty [IsEmpty α] : s.chainHeight = 0 :=
  chainHeight_eq_zero_iff.mpr (Subsingleton.elim _ _)

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

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

Разделы

Аффилиация

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