ι : Type ?u.10515
R : Type ?u.10518
R' : Type ?u.10521
E : Type u_1
F : Type u_2
G : Type ?u.10530
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ ↑f (x + -y) ≤ max (↑f x) (↑f (-y))
ι : Type ?u.10515
R : Type ?u.10518
R' : Type ?u.10521
E : Type u_1
F : Type u_2
G : Type ?u.10530
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ ↑f (x - y) ≤ max (↑f x) (↑f y)
rw [sub_eq_add_neg, ← NonarchAddGroupSeminormClass.map_neg_eq_map' f y]
no goals
ι : Type ?u.10515
R : Type ?u.10518
R' : Type ?u.10521
E : Type u_1
F : Type u_2
G : Type ?u.10530
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ ↑f (x + -y) ≤ max (↑f x) (↑f (-y))
exact map_add_le_max _ _ _