liftOrderTop — Mathlib

English

Given a Galois connection, one can lift the top element from β to α via the right adjoint, producing an OrderTop on α.

Русский

Дана связь Галуа; верхний элемент β поднимается в α через правый смежный отображатель, порождая порядок-верхний на α.

LaTeX

$$$\\text{If } gc : GaloisConnection l\\,u \\text{ and } β \\text{ has a top, then } α \\text{ inherits a top } u(\\top_β).$$$

Lean4

/-- Lift the top along a Galois connection -/
def liftOrderTop {α β : Type*} [PartialOrder α] [Preorder β] [OrderTop β] {l : α → β} {u : β → α}
    (gc : GaloisConnection l u) : OrderTop α where
  top := u ⊤
  le_top _ := gc.le_u <| le_top

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