theorem enorm_multiset_sum_le {E : Type u_2} [TopologicalSpace E] [ENormedAddCommMonoid E] (m : Multiset E) : ‖m.sum‖ₑ ≤ (Multiset.map (fun (x : E) => ‖x‖ₑ) m).sum

theorem enorm_multiset_prod_le {E : Type u_2} [TopologicalSpace E] [ENormedCommMonoid E] (m : Multiset E) : ‖m.prod‖ₑ ≤ (Multiset.map (fun (x : E) => ‖x‖ₑ) m).sum

theorem enorm_sum_le {ι : Type u_1} {E : Type u_2} [TopologicalSpace E] [ENormedAddCommMonoid E] (s : Finset ι) (f : ι → E) : ‖∑ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ

theorem enorm_prod_le {ι : Type u_1} {E : Type u_2} [TopologicalSpace E] [ENormedCommMonoid E] (s : Finset ι) (f : ι → E) : ‖∏ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ

theorem enorm_prod_le_of_le {ι : Type u_1} {E : Type u_2} [TopologicalSpace E] [ENormedCommMonoid E] (s : Finset ι) {f : ι → E} {n : ι → ENNReal} (h : ∀ b ∈ s, ‖f b‖ₑ ≤ n b) : ‖∏ b ∈ s, f b‖ₑ ≤ ∑ b ∈ s, n b

theorem enorm_sum_le_of_le {ι : Type u_1} {E : Type u_2} [TopologicalSpace E] [ENormedAddCommMonoid E] (s : Finset ι) {f : ι → E} {n : ι → ENNReal} (h : ∀ b ∈ s, ‖f b‖ₑ ≤ n b) : ‖∑ b ∈ s, f b‖ₑ ≤ ∑ b ∈ s, n b