Theorems · Definition · order theory

GaloisInsertion.monotoneIntro

{α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {l : α → β} →
          {u : β → α} →
            Monotone u → Monotone l → (∀ (a : α), a ≤ u (l a)) → (∀ (b : β), l (u b) = b) → GaloisInsertion l u

A constructor for a Galois insertion with the trivial choice function.

Defined in

Mathlib.Order.GaloisConnection.Defs

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

PreorderPreorder