instCompleteSemilatticeInfElemFixedPointsCoeOrderHom

English

Knaster–Tarski: The set of fixed points Fix(f) of a monotone f on a complete lattice forms a complete lattice, with top equal to the greatest fixed point and bottom equal to the least fixed point.

Русский

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

LaTeX

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

Lean4

instance : CompleteSemilatticeInf (fixedPoints f) :=
  {
    Subtype.partialOrder
      _ with
    sInf := fun s =>
      f.prevFixed (sInf (Subtype.val '' s))
        (f.map_sInf_subset_fixedPoints_le (Subtype.val '' s) fun _ ⟨x, hx⟩ => hx.2 ▸ x.2)
    le_sInf := fun _ _ hx => f.le_prevFixed _ <| le_sInf <| Set.forall_mem_image.2 hx
    sInf_le := fun _ _ hx =>
      Subtype.coe_le_coe.1 <| le_trans (f.prevFixed_le _) (sInf_le <| Set.mem_image_of_mem _ hx) }

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