𝓕 : Type ?u.1102052
𝕜 : Type ?u.1102055
α : Type ?u.1102058
ι : Type ?u.1102061
κ : Type ?u.1102064
E : Type u_1
F : Type ?u.1102070
G : Type ?u.1102073
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : Multiset E
⊢ ‖Multiset.prod m‖ ≤ Multiset.sum (Multiset.map toReal (Multiset.map (fun x => ‖x‖₊) m))
𝓕 : Type ?u.1102052
𝕜 : Type ?u.1102055
α : Type ?u.1102058
ι : Type ?u.1102061
κ : Type ?u.1102064
E : Type u_1
F : Type ?u.1102070
G : Type ?u.1102073
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : Multiset E
⊢ ↑‖Multiset.prod m‖₊ ≤ ↑(Multiset.sum (Multiset.map (fun x => ‖x‖₊) m))
push_cast
𝓕 : Type ?u.1102052
𝕜 : Type ?u.1102055
α : Type ?u.1102058
ι : Type ?u.1102061
κ : Type ?u.1102064
E : Type u_1
F : Type ?u.1102070
G : Type ?u.1102073
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : Multiset E
⊢ ‖Multiset.prod m‖ ≤ Multiset.sum (Multiset.map (toReal ∘ fun x => ‖x‖₊) m)
𝓕 : Type ?u.1102052
𝕜 : Type ?u.1102055
α : Type ?u.1102058
ι : Type ?u.1102061
κ : Type ?u.1102064
E : Type u_1
F : Type ?u.1102070
G : Type ?u.1102073
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : Multiset E
⊢ ‖Multiset.prod m‖ ≤ Multiset.sum (Multiset.map toReal (Multiset.map (fun x => ‖x‖₊) m))
rw [Multiset.map_map]
no goals
𝓕 : Type ?u.1102052
𝕜 : Type ?u.1102055
α : Type ?u.1102058
ι : Type ?u.1102061
κ : Type ?u.1102064
E : Type u_1
F : Type ?u.1102070
G : Type ?u.1102073
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
m : Multiset E
⊢ ‖Multiset.prod m‖ ≤ Multiset.sum (Multiset.map (toReal ∘ fun x => ‖x‖₊) m)
exact norm_multiset_prod_le _