Theorems · Theorem · order theory

SupHomClass.map_sup

∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Max α} {inst_1 : Max β} {inst_2 : FunLike F α β}
  [self : SupHomClass F α β] (f : F) (a b : α), f (a ⊔ b) = f a ⊔ f b

A SupHomClass morphism preserves suprema.

Defined in

Mathlib.Order.Hom.Lattice

Cited by

20 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

SupHomClass