English
If t is bounded between o1 and o2, nil is bounded between x and o2, and all elements of t are > x, then t is bounded between o1 and o2 with x as a lower bound.
Русский
Если дерево t ограничено между o1 и o2, nil ограничено между x и o2 и все элементы t больше x, тогда t ограничено между o1 и o2 с x в качестве нижней границы.
LaTeX
$$$\forall t\ o_1\ o_2\ x: (Bounded\ t\ o_1\ o_2) \land (Bounded\ nil\ x\ o_2) \land (All(> x)\ t) \Rightarrow Bounded\ t\ o_1\ o_2$$$
Lean4
theorem of_gt : ∀ {t o₁ o₂} {x : α}, Bounded t o₁ o₂ → Bounded nil x o₂ → All (· > x) t → Bounded t x o₂
| nil, _, _, _, _, hn, _ => hn
| node _ _ _ _, _, _, _, ⟨h₁, h₂⟩, _, ⟨al₁, al₂, _⟩ => ⟨h₁.of_gt al₂ al₁, h₂⟩
