Theorems · Theorem · order theory

SubadditiveHomClass.map_add_le_add

∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Add α} {inst_1 : Add β} {inst_2 : LE β}
  {inst_3 : FunLike F α β} [self : SubadditiveHomClass F α β] (f : F) (a b : α), f (a + b) ≤ f a + f b

the image of a sum is less or equal than the sum of the images.

Defined in

Mathlib.Algebra.Order.Hom.Basic

Cited by

11 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

SubadditiveHomClass