map_sInf_subset_fixedPoints_le — Mathlib

English

Let f be an order-preserving endomorphism of a complete lattice and A a subset of fixed points of f. Then the infimum of A is a pre-fixed point, i.e., f(inf A) ≤ inf A.

Русский

Пусть f — монотонное отображение на полной решётке и A ⊆ Fix(f). Тогда inf A удовлетворяет f(inf A) ≤ inf A.

LaTeX

$$$$f(\\operatorname{Inf} A) \\le \\operatorname{Inf} A$$$$

Lean4

theorem map_sInf_subset_fixedPoints_le (A : Set α) (hA : A ⊆ fixedPoints f) : f (sInf A) ≤ sInf A :=
  le_sInf fun _ hx => hA hx ▸ (f.mono <| sInf_le hx)

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