Theorems · Theorem · order theory

LowerAdjoint.mk.inj

∀ {α : Type u_1} {β : Type u_4} {inst : Preorder α} {inst_1 : Preorder β} {u : β → α} {toFun : α → β}
  {gc' : GaloisConnection toFun u} {toFun_1 : α → β} {gc'_1 : GaloisConnection toFun_1 u},
  { toFun := toFun, gc' := gc' } = { toFun := toFun_1, gc' := gc'_1 } → toFun = toFun_1

Defined in

Mathlib.Order.Closure

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms