Theorems · Theorem · order theory

GaloisInsertion.gc

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

The Galois connection associated to a Galois insertion.

Defined in

Mathlib.Order.GaloisConnection.Defs

Cited by

137 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 7 definitions · uses no axioms

Assumes

PreorderPreorder