𝓕 : Type ?u.739254
𝕜 : Type ?u.739257
α : Type ?u.739260
ι : Type u_1
κ : Type ?u.739266
E : Type u_2
F : Type ?u.739272
G : Type ?u.739275
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ (b : ι), b ∈ s → ‖f b / a b‖ ≤ d b
⊢ ‖∏ x in s, f x / a x‖ ≤ ∑ b in s, d b
𝓕 : Type ?u.739254
𝕜 : Type ?u.739257
α : Type ?u.739260
ι : Type u_1
κ : Type ?u.739266
E : Type u_2
F : Type ?u.739272
G : Type ?u.739275
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ (b : ι), b ∈ s → dist (f b) (a b) ≤ d b
⊢ dist (∏ b in s, f b) (∏ b in s, a b) ≤ ∑ b in s, d b
simp only [dist_eq_norm_div, ← Finset.prod_div_distrib] at *
no goals
𝓕 : Type ?u.739254
𝕜 : Type ?u.739257
α : Type ?u.739260
ι : Type u_1
κ : Type ?u.739266
E : Type u_2
F : Type ?u.739272
G : Type ?u.739275
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ (b : ι), b ∈ s → ‖f b / a b‖ ≤ d b
⊢ ‖∏ x in s, f x / a x‖ ≤ ∑ b in s, d b
exact norm_prod_le_of_le s h