ι : Type ?u.44336
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.44348
δ : Type ?u.44351
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommGroup β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f x ≤ ↑f y + ↑f (x / y) ∧ ↑f y ≤ ↑f x + ↑f (x / y)
ι : Type ?u.44336
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.44348
δ : Type ?u.44351
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommGroup β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ abs (↑f x - ↑f y) ≤ ↑f (x / y)
rw [abs_sub_le_iff, sub_le_iff_le_add', sub_le_iff_le_add']
no goals
ι : Type ?u.44336
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.44348
δ : Type ?u.44351
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommGroup β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f x ≤ ↑f y + ↑f (x / y) ∧ ↑f y ≤ ↑f x + ↑f (x / y)
exact ⟨le_map_add_map_div _ _ _, le_map_add_map_div' _ _ _⟩