of_lt — Mathlib

English

If t is bounded between o1 and o2, and nil is bounded between o1 and x, and all elements of t are < x, then t is bounded between o1 and x.

Русский

Если дерево t ограничено между o1 и o2, и nil ограничено между o1 и x, и все элементы t меньше x, тогда t ограничено между o1 и x.

LaTeX

$$$\forall t\ o_1\ o_2\ x: (Bounded\ t\ o_1\ o_2) \land (Bounded\ nil\ o_1\ x) \land (All(\cdot < x)\ t) \Rightarrow Bounded\ t\ o_1\ x$$$

Lean4

theorem of_lt : ∀ {t o₁ o₂} {x : α}, Bounded t o₁ o₂ → Bounded nil o₁ x → All (· < x) t → Bounded t o₁ x
  | nil, _, _, _, _, hn, _ => hn
  | node _ _ _ _, _, _, _, ⟨h₁, h₂⟩, _, ⟨_, al₂, al₃⟩ => ⟨h₁, h₂.of_lt al₂ al₃⟩

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