le_map_sSup_subset_fixedPoints — Mathlib

English

Let f be an order-preserving endomorphism of a complete lattice and A a subset of fixed points of f. Then the supremum of A is a post-fixed point, i.e., f(sup A) ≥ sup A.

Русский

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

LaTeX

$$$$f(\\operatorname{sSup} A) \\ge \\operatorname{sSup} A$$$$

Lean4

theorem le_map_sSup_subset_fixedPoints (A : Set α) (hA : A ⊆ fixedPoints f) : sSup A ≤ f (sSup A) :=
  sSup_le fun _ hx => hA hx ▸ (f.mono <| le_sSup hx)

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