monotoneIntro — Mathlib

English

Construct a bottom for β by mapping the bottom of α via l: bot_β = l(bot_α).

Русский

Построить нижнюю грань β как l(⊥_α).

LaTeX

$$$$ \text{bot}_{\beta} = l(\bot_{\alpha}). $$$$

Lean4

/-- A constructor for a Galois insertion with the trivial `choice` function. -/
def monotoneIntro {α β : Type*} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (hu : Monotone u) (hl : Monotone l)
    (hul : ∀ a, a ≤ u (l a)) (hlu : ∀ b, l (u b) = b) : GaloisInsertion l u
    where
  choice x _ := l x
  gc := GaloisConnection.monotone_intro hu hl hul fun b => le_of_eq (hlu b)
  le_l_u b := le_of_eq <| (hlu b).symm
  choice_eq _ _ := rfl

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