toGaloisInsertion — Mathlib

English

In a Galois insertion, l(u(b)) = b for all b.

Русский

В связке Галуаl-u выполняется l(u(b)) = b для всех b.

LaTeX

$$$$ l(u(b)) = b $$$$

Lean4

/-- Make a `GaloisInsertion l u` from a `GaloisConnection l u` such that `∀ b, b ≤ l (u b)` -/
def toGaloisInsertion {α β : Type*} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u)
    (h : ∀ b, b ≤ l (u b)) : GaloisInsertion l u :=
  { choice := fun x _ => l x
    gc
    le_l_u := h
    choice_eq := fun _ _ => rfl }

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