𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁷ : Fintype ι
inst✝¹⁶ : Fintype ι'
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹² : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝¹⁰ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁹ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁸ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
c : 𝕜
f✝ g✝ : ContinuousMultilinearMap 𝕜 E G
m✝ : (i : ι) → E i
𝕜' : Type ?u.552038
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' G
inst✝ : SMulCommClass 𝕜 𝕜' G
f : ContinuousMultilinearMap 𝕜 E G
g : ContinuousMultilinearMap 𝕜 E G'
m : (i : ι) → E i
H : 0 ≤ ∏ i : ι, ‖m i‖
⊢ ‖↑(prod f g) m‖ ≤ max ‖f‖ ‖g‖ * ∏ i : ι, ‖m i‖
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁷ : Fintype ι
inst✝¹⁶ : Fintype ι'
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹² : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝¹⁰ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁹ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁸ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
c : 𝕜
f✝ g✝ : ContinuousMultilinearMap 𝕜 E G
m✝ : (i : ι) → E i
𝕜' : Type ?u.552038
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' G
inst✝ : SMulCommClass 𝕜 𝕜' G
f : ContinuousMultilinearMap 𝕜 E G
g : ContinuousMultilinearMap 𝕜 E G'
m : (i : ι) → E i
⊢ ‖↑(prod f g) m‖ ≤ max ‖f‖ ‖g‖ * ∏ i : ι, ‖m i‖
have H : 0 ≤ ∏ i, ‖m i‖ := prod_nonneg fun _ _ => norm_nonneg _
no goals
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁷ : Fintype ι
inst✝¹⁶ : Fintype ι'
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹² : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝¹⁰ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁹ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁸ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
c : 𝕜
f✝ g✝ : ContinuousMultilinearMap 𝕜 E G
m✝ : (i : ι) → E i
𝕜' : Type ?u.552038
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' G
inst✝ : SMulCommClass 𝕜 𝕜' G
f : ContinuousMultilinearMap 𝕜 E G
g : ContinuousMultilinearMap 𝕜 E G'
m : (i : ι) → E i
H : 0 ≤ ∏ i : ι, ‖m i‖
⊢ ‖↑(prod f g) m‖ ≤ max ‖f‖ ‖g‖ * ∏ i : ι, ‖m i‖
simpa only [prod_apply, Prod.norm_def, max_mul_of_nonneg, H] using
  max_le_max (f.le_op_norm m) (g.le_op_norm m)