𝓕 : Type ?u.86263
𝕜 : Type ?u.86266
α : Type ?u.86269
ι : Type ?u.86272
κ : Type ?u.86275
E : Type u_1
F : Type ?u.86281
G : Type ?u.86284
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : E
⊢ ‖v‖ ≤ ‖u‖ + ‖v / u‖
𝓕 : Type ?u.86263
𝕜 : Type ?u.86266
α : Type ?u.86269
ι : Type ?u.86272
κ : Type ?u.86275
E : Type u_1
F : Type ?u.86281
G : Type ?u.86284
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : E
⊢ ‖v‖ ≤ ‖u‖ + ‖u / v‖
rw [norm_div_rev]
no goals
𝓕 : Type ?u.86263
𝕜 : Type ?u.86266
α : Type ?u.86269
ι : Type ?u.86272
κ : Type ?u.86275
E : Type u_1
F : Type ?u.86281
G : Type ?u.86284
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : E
⊢ ‖v‖ ≤ ‖u‖ + ‖v / u‖
exact norm_le_norm_add_norm_div' v u