chainHeight_insert_of_forall_lt — Mathlib

English

If a is less than every element of s, then inserting a into s increases chainHeight by 1.

Русский

Если a меньше любого элемента s, добавление a в s увеличивает цепную высоту на 1.

LaTeX

$$∀ {s : Set α} [Preorder α] (a : α) (ha : ∀ b ∈ s, b < a), (insert a s).chainHeight = s.chainHeight + 1$$

Lean4

theorem chainHeight_insert_of_forall_lt (a : α) (ha : ∀ b ∈ s, b < a) : (insert a s).chainHeight = s.chainHeight + 1 :=
  by
  rw [← chainHeight_dual, ← chainHeight_dual s]
  exact chainHeight_insert_of_forall_gt _ ha

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