weak_right — Mathlib

English

If a tree t is bounded between o1 and o2, then it remains bounded between o1 and ⊤ when the right bound is weakened to ⊤.

Русский

Если дерево t ограничено между o1 и o2, то при ослаблении правой границы до ⊤ дерево сохраняет ограниченность между o1 и ⊤.

LaTeX

$$$\forall t\ o_1\ o_2: Bounded\ t\ o_1\ o_2 \Rightarrow Bounded\ t\ o_1\ top$$$

Lean4

theorem weak_right : ∀ {t : Ordnode α} {o₁ o₂}, Bounded t o₁ o₂ → Bounded t o₁ ⊤
  | nil, o₁, o₂, h => by cases o₁ <;> trivial
  | node _ _ _ _, _, _, ⟨ol, Or⟩ => ⟨ol, Or.weak_right⟩

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