chainHeight_empty — Mathlib

English

Let α be a type with a given order. The chainHeight of the empty set is zero: the height of ∅ inside Set α is 0.

Русский

Пусть α—это множество с заданным порядком. Цепная высота пустого множества равна нулю: chainHeight(∅) = 0 для множества в α.

LaTeX

$$$ (\\varnothing : Set\\,\\alpha).chainHeight = 0 $$$

Lean4

@[simp]
theorem chainHeight_empty : (∅ : Set α).chainHeight = 0 :=
  chainHeight_eq_zero_iff.2 rfl

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