Theorems · Theorem · order theory

TopHomClass.map_top

∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : Top α} {inst_1 : Top β}
  {inst_2 : FunLike F α β} [self : TopHomClass F α β] (f : F), f ⊤ = ⊤

A TopHomClass morphism preserves the top element.

Defined in

Mathlib.Order.Hom.Bounded

Cited by

14 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

TopHomClass