le_map_sup_fixedPoints — Mathlib

English

Let f be an order-preserving map on a complete lattice. If x and y are fixed points of f (i.e., f(x) = x and f(y) = y), then x ∨ y satisfies x ∨ y ≤ f(x ∨ y).

Русский

Пусть f — монотонное отображение на полной решётке. Пусть x и y — фиксированные точки f (f(x) = x, f(y) = y). Тогда их объединение x ∨ y удовлетворяет неравенству x ∨ y ≤ f(x ∨ y).

LaTeX

$$$$(x\\vee y) \\le f(x\\vee y)$$$$

Lean4

theorem le_map_sup_fixedPoints (x y : fixedPoints f) : (x ⊔ y : α) ≤ f (x ⊔ y) :=
  calc
    (x ⊔ y : α) = f x ⊔ f y := congr_arg₂ (· ⊔ ·) x.2.symm y.2.symm
    _ ≤ f (x ⊔ y) := f.mono.le_map_sup x y

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