𝓕 : Type ?u.1102940
𝕜 : Type ?u.1102943
α : Type ?u.1102946
ι : Type u_1
κ : Type ?u.1102952
E : Type u_2
F : Type ?u.1102958
G : Type ?u.1102961
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f : ι → E
⊢ ‖∏ a in s, f a‖ ≤ ∑ x in s, ‖f x‖
𝓕 : Type ?u.1102940
𝕜 : Type ?u.1102943
α : Type ?u.1102946
ι : Type u_1
κ : Type ?u.1102952
E : Type u_2
F : Type ?u.1102958
G : Type ?u.1102961
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f : ι → E
⊢ ↑‖∏ a in s, f a‖₊ ≤ ↑(∑ a in s, ‖f a‖₊)
push_cast
no goals
𝓕 : Type ?u.1102940
𝕜 : Type ?u.1102943
α : Type ?u.1102946
ι : Type u_1
κ : Type ?u.1102952
E : Type u_2
F : Type ?u.1102958
G : Type ?u.1102961
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
s : Finset ι
f : ι → E
⊢ ‖∏ a in s, f a‖ ≤ ∑ x in s, ‖f x‖
exact norm_prod_le _ _