instCompleteSemilatticeSupElemFixedPointsCoeOrderHom

English

The fixed points of f form a complete semilattice under the inherited order, with compatible suprema and infima defined by the ambient lattice and lifting to fixed points.

Русский

Фиксированные точки f образуют полную полуправлю (полную полуправляющую лодку) по унаследованному порядку; операции максимума и минимума поднимаются из исходной решётки к фиксированным точкам.

LaTeX

$$$$\\mathrm{Fix}(f) \\text{ is a complete semilattice under the inherited order}$$$$

Lean4

instance : CompleteSemilatticeSup (fixedPoints f) :=
  {
    Subtype.partialOrder
      _ with
    sSup := fun s =>
      f.nextFixed (sSup (Subtype.val '' s))
        (f.le_map_sSup_subset_fixedPoints (Subtype.val '' s) fun _ ⟨x, hx⟩ => hx.2 ▸ x.2)
    le_sSup := fun _ _ hx => Subtype.coe_le_coe.1 <| le_trans (le_sSup <| Set.mem_image_of_mem _ hx) (f.le_nextFixed _)
    sSup_le := fun _ _ hx => f.nextFixed_le _ <| sSup_le <| Set.forall_mem_image.2 hx }

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