instSemilatticeSupElemFixedPointsCoeOrderHom

English

The fixed points of an order-homomorphism form a semilattice with inf defined by taking the fixed point above x ∧ y; this is the meet in Fix(f).

Русский

Фиксированные точки отображения, сохранённого порядка, образуют полуправлю (полуполе) с операцией Meet, определяемой как наименьшая фиксированная точка, не меньшая чем x ∧ y.

LaTeX

$$$$\\text{Inf}_{\\mathrm{Fix}(f)}(x,y) = \\text{the least fixed point above } (x \\wedge y)$$$$

Lean4

instance : SemilatticeSup (fixedPoints f) :=
  {
    Subtype.partialOrder
      _ with
    sup := fun x y => f.nextFixed (x ⊔ y) (f.le_map_sup_fixedPoints x y)
    le_sup_left := fun _ _ => Subtype.coe_le_coe.1 <| le_sup_left.trans (f.le_nextFixed _)
    le_sup_right := fun _ _ => Subtype.coe_le_coe.1 <| le_sup_right.trans (f.le_nextFixed _)
    sup_le := fun _ _ _ hxz hyz => f.nextFixed_le _ <| sup_le hxz hyz }

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