mono_right — Mathlib

English

If x ≤ y, then increasing the right bound from x to y preserves boundedness: if t is bounded by x on the right, then it is bounded by y on the right with the same left bound.

Русский

Если x ≤ y, то увеличение правой границы с x до y сохраняет ограниченность: если t ограничено справа x, то ограничение справа становится y.

LaTeX

$$$\forall x\, y\ (xy:\ x \le y),\forall t\ o,\ t.Bounded\ o\ x\ o \Rightarrow t.Bounded\ o\ y\ o$$$

Lean4

theorem mono_right {x y : α} (xy : x ≤ y) : ∀ {t : Ordnode α} {o}, Bounded t o x → Bounded t o y
  | nil, none, _ => ⟨⟩
  | nil, some _, h => lt_of_lt_of_le h xy
  | node _ _ _ _, _o, ⟨ol, or⟩ => ⟨ol, or.mono_right xy⟩

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