Theorems · Definition · order theory

GaloisConnection.toGaloisInsertion

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

Make a GaloisInsertion l u from a GaloisConnection l u such that ∀ b, b ≤ l (u b)

Defined in

Mathlib.Order.GaloisConnection.Defs

Cited by

0 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

PreorderPreorder