liftOrderTop — Mathlib

English

There is a top element on β given by topβ = l(topα) provided by the adjunction, ensuring top(β) is above all β-elements.

Русский

Существует верхний элемент в β, заданный как topβ = l(topα), обеспечиваемый аксиомой сопряженности.

LaTeX

$$$$ \text{top}_{β} = l(\text{top}_{α}), \; \text{le}_{β}(x, \text{top}_{β}) \text{ holds for all } x. $$$$

Lean4

/-- Lift the top along a Galois insertion -/
abbrev liftOrderTop [Preorder α] [OrderTop α] (gi : GaloisInsertion l u) : OrderTop β
    where
  top := gi.choice ⊤ <| le_top
  le_top := by simp only [gi.choice_eq];
    exact fun b =>
      (gi.le_l_u b).trans
        (gi.gc.monotone_l le_top)
          -- See note [reducible non-instances]

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