completeLattice — Mathlib

English

Let f be an order-preserving endomorphism of a complete lattice. Then Fix(f) is a complete lattice with order inherited from the ambient lattice; top is the greatest fixed point and bottom the least fixed point.

Русский

Пусть f — монотонное отображение на полной решётке. Тогда Fix(f) образует полную решётку, порядок которой наследуется от исходной; верхняя граница — наибольшая фиксированная точка, нижняя — наименьшая фиксированная точка.

LaTeX

$$$$\\text{Fix}(f) \\text{ is a complete lattice with top }= \\mathrm{gfp}(f) \\text{ and bottom }= \\mathrm{lfp}(f).$$$$

Lean4

/-- **Knaster-Tarski Theorem**: The fixed points of `f` form a complete lattice. -/
instance completeLattice : CompleteLattice (fixedPoints f)
    where
  __ := inferInstanceAs (SemilatticeInf (fixedPoints f))
  __ := inferInstanceAs (SemilatticeSup (fixedPoints f))
  __ := inferInstanceAs (CompleteSemilatticeInf (fixedPoints f))
  __ := inferInstanceAs (CompleteSemilatticeSup (fixedPoints f))
  top := ⟨f.gfp, f.isFixedPt_gfp⟩
  bot := ⟨f.lfp, f.isFixedPt_lfp⟩
  le_top x := f.le_gfp x.2.ge
  bot_le x := f.lfp_le x.2.le

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