English
There is a construction of a Galois coinsertion from monotone maps l and u with trivial choice by dualizing a monotone insertion.
Русский
Существует конструктор коинсерции Галуа из монотонных отображений l и u с тривиальным выбором, получаемый через дуализацию вставки.
LaTeX
$$$\\text{If } l,u \\text{ are monotone and satisfy } l(u(b)) \\le b \\text{ and } u(l(a)) = a, \\text{ then } \\text{GaloisCoinsertion } l\\,u \\text{ exists.}$$$
Lean4
/-- A constructor for a Galois coinsertion with the trivial `choice` function. -/
def monotoneIntro [Preorder α] [Preorder β] {l : α → β} {u : β → α} (hu : Monotone u) (hl : Monotone l)
(hlu : ∀ b, l (u b) ≤ b) (hul : ∀ a, u (l a) = a) : GaloisCoinsertion l u :=
(GaloisInsertion.monotoneIntro hl.dual hu.dual hlu hul).ofDual
