mono_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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