mono_right — Mathlib

English

Let α be a preorder. If x ≤ y and a tree t is valid under o with top bound x, then t is valid under top bound y.

Русский

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

LaTeX

$$$\\forall \\alpha [Preorder(\\alpha)], \\forall x,y,t,o:\\; x \\le y \\Rightarrow (Ordnode.Valid'(o, t, x) \\Rightarrow Ordnode.Valid'(o, t, y)).$$$

Lean4

theorem mono_right {x y : α} (xy : x ≤ y) {t : Ordnode α} {o} (h : Valid' o t x) : Valid' o t y :=
  ⟨h.1.mono_right xy, h.2, h.3⟩

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