mono_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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