map_inf_fixedPoints_le — Mathlib

English

Let f be an order-preserving endomorphism of a complete lattice. If x and y are fixed points of f, then f(x ∧ y) ≤ x ∧ y, i.e., the meet of fixed points is below its image.

Русский

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

LaTeX

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

Lean4

theorem map_inf_fixedPoints_le (x y : fixedPoints f) : f (x ⊓ y) ≤ x.val ⊓ y.val :=
  f.dual.le_map_sup_fixedPoints x y

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