Theorems · Theorem · order theory

NonnegHomClass.apply_nonneg

∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Zero β} {inst_1 : LE β}
  {inst_2 : FunLike F α β} [self : NonnegHomClass F α β] (f : F) (a : α), 0 ≤ f a

the image of any element is nonnegative.

Defined in

Mathlib.Algebra.Order.Hom.Basic

Cited by

79 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

NonnegHomClass