Theorems · Definition · order theory

TopHomClass.toTopHom

{F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} → [inst : FunLike F α β] → [inst_1 : Top α] → [inst_2 : Top β] → [TopHomClass F α β] → F → TopHom α β

Turn an element of a type F satisfying TopHomClass F α β into an actual TopHom. This is declared as the default coercion from F to TopHom α β.

Defined in

Mathlib.Order.Hom.Bounded

Cited by

1 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

FunLikeTopTopTopHomClass