Mathlib Map

Theorems · Definition · order theory

LowerAdjoint.toFun

{α : Type u_1} → {β : Type u_4} → [inst : Preorder α] → [inst_1 : Preorder β] → {u : β → α} → LowerAdjoint u → α → β

The underlying function

Defined in
Mathlib.Order.Closure
Cited by
105 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Assumes
PreorderPreorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

FirstOrder.Language.Substructure.FG · cited by 34Substructure.FGFirstOrder.Language.Substructure.CG · cited by 18Substructure.CGLowerAdjoint.closureOperator · cited by 12LowerAdjoint.closureOpera…FirstOrder.Language.Substructure.subset_closure · cited by 12Substructure.subset_closu…LowerAdjoint.closed · cited by 9LowerAdjoint.closedFirstOrder.Language.Substructure.closure_eq · cited by 7Substructure.closure_eqFirstOrder.Language.Substructure.closure_le · cited by 7Substructure.closure_leFirstOrder.Language.Substructure.fg_def · cited by 6Substructure.fg_defFirstOrder.Language.Substructure.cg_def · cited by 5Substructure.cg_defFirstOrder.Language.Substructure.closure_eq_of_le · cited by 5Substructure.closure_eq_o…FirstOrder.Language.Substructure.FG.sup · cited by 5FG.supFirstOrder.Language.Substructure.closure_image · cited by 4Substructure.closure_imageFirstOrder.Language.Substructure.closure_union · cited by 4Substructure.closure_unionFirstOrder.Language.Substructure.fg_closure_singleton · cited by 4Substructure.fg_closure_s…FirstOrder.Language.Substructure.gi · cited by 4Substructure.giPreorder · cited by 7952PreorderLowerAdjoint · cited by 38LowerAdjointLowerAdjoint.toFunCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by112

Results whose statement or proof uses this declaration.