trans_right — Mathlib

English

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

Русский

Если t1 ограничено слева o1 и справа x, а t2 ограничено слева x и справа o2, то t1 ограничено между 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_1.Bounded\ o_1\ o_2)$$$

Lean4

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

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