toGaloisCoinsertion — Mathlib

English

From a Galois connection gc and a bound u(l a) ≤ a for all a, create a GaloisCoinsertion l u.

Русский

Из связки Галуа gc и условия u(l(a)) ≤ a для всех a строится коинсерция Галуа l,u.

LaTeX

$$$\\text{If } gc : \\text{GaloisConnection } l\\,u \\text{ and } \\forall a, u(l(a)) \\le a, \\text{ then } GaloisCoinsertion\\,l\\,u.$$$

Lean4

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

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