weak_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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