trans_left — Mathlib

English

If t1 is bounded by o1 on the left and by x on the right, and t2 is bounded by x on the left and by o2 on the right, then t2 is bounded between o1 and o2.

Русский

Если t1 ограничено слева o1 и справа x, а t2 ограничено слева x и справа o2, то t2 ограничено между o1 и o2.

LaTeX

$$$\forall t_1\ t_2\ x\ o_1\ o_2: (t_1.Bounded\ o_1\ x) \land (t_2.Bounded\ x\ o_2) \Rightarrow (t_2.Bounded\ o_1\ o_2)$$$

Lean4

theorem trans_left {t₁ t₂ : Ordnode α} {x : α} : ∀ {o₁ o₂}, Bounded t₁ o₁ x → Bounded t₂ x o₂ → Bounded t₂ o₁ o₂
  | none, _, _, h₂ => h₂.weak_left
  | some _, _, h₁, h₂ => h₂.mono_left (le_of_lt h₁.to_lt)

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