Theorems · Definition · order theory

SupHom.toFun

{α : Type u_6} → {β : Type u_7} → [inst : Max α] → [inst_1 : Max β] → SupHom α β → α → β

The underlying function of a SupHom. Do not use this function directly. Instead use the coercion coming from the FunLike instance.

Defined in

Mathlib.Order.Hom.Lattice

Cited by

43 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

MaxMax