F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.37806
δ : Type ?u.37809
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : Monotone ↑f
a : α
⊢ 0 ≤ a → ↑f 0 ≤ ↑f a
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.37806
δ : Type ?u.37809
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : Monotone ↑f
a : α
⊢ 0 ≤ a → 0 ≤ ↑f a
rw [← map_zero f]
no goals
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.37806
δ : Type ?u.37809
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : Monotone ↑f
a : α
⊢ 0 ≤ a → ↑f 0 ≤ ↑f a
apply h
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.37806
δ : Type ?u.37809
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : ∀ (a : α), 0 ≤ a → 0 ≤ ↑f a
a b : α
hl : a ≤ b
⊢ ↑f a ≤ ↑f (b - a) + ↑f a
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.37806
δ : Type ?u.37809
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : ∀ (a : α), 0 ≤ a → 0 ≤ ↑f a
a b : α
hl : a ≤ b
⊢ ↑f a ≤ ↑f b
rw [← sub_add_cancel b a, map_add f]
no goals
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.37806
δ : Type ?u.37809
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : ∀ (a : α), 0 ≤ a → 0 ≤ ↑f a
a b : α
hl : a ≤ b
⊢ ↑f a ≤ ↑f (b - a) + ↑f a
exact le_add_of_nonneg_left (h _ <| sub_nonneg.2 hl)