𝕜 : 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'
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖↑(↑f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
⊢ ‖mkContinuous
        {
          toFun := fun m =>
            mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
              (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖),
          map_add' :=
            (_ :
              ∀ [inst : DecidableEq ι] (m : (i : ι) → E i) (i : ι) (x y : E i),
                (fun m =>
                      mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                        (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                    (Function.update m i (x + y)) =
                  (fun m =>
                        mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                          (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                      (Function.update m i x) +
                    (fun m =>
                        mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                          (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                      (Function.update m i y)),
          map_smul' :=
            (_ :
              ∀ [inst : DecidableEq ι] (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
                (fun m =>
                      mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                        (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                    (Function.update m i (c • x)) =
                  c •
                    (fun m =>
                        mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                          (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                      (Function.update m i x)) }
        (max C 0)
        (_ :
          ∀ (m : (i : ι) → E i),
            ‖↑{
                      toFun := fun m =>
                        mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                          (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖),
                      map_add' :=
                        (_ :
                          ∀ [inst : DecidableEq ι] (m : (i : ι) → E i) (i : ι) (x y : E i),
                            (fun m =>
                                  mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                                    (_ :
                                      ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                                (Function.update m i (x + y)) =
                              (fun m =>
                                    mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                                      (_ :
                                        ∀ (m₂ : (i : ι') → E' i),
                                          ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                                  (Function.update m i x) +
                                (fun m =>
                                    mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                                      (_ :
                                        ∀ (m₂ : (i : ι') → E' i),
                                          ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                                  (Function.update m i y)),
                      map_smul' :=
                        (_ :
                          ∀ [inst : DecidableEq ι] (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
                            (fun m =>
                                  mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                                    (_ :
                                      ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                                (Function.update m i (c • x)) =
                              c •
                                (fun m =>
                                    mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                                      (_ :
                                        ∀ (m₂ : (i : ι') → E' i),
                                          ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                                  (Function.update m i x)) }
                  m‖ ≤
              max C 0 * ∏ i : ι, ‖m i‖)‖ ≤
    max C 0
𝕜 : 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'
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖↑(↑f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
⊢ ‖mkContinuousMultilinear f C H‖ ≤ max C 0
dsimp only [mkContinuousMultilinear]
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'
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖↑(↑f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
⊢ ‖mkContinuous
        {
          toFun := fun m =>
            mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
              (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖),
          map_add' :=
            (_ :
              ∀ [inst : DecidableEq ι] (m : (i : ι) → E i) (i : ι) (x y : E i),
                (fun m =>
                      mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                        (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                    (Function.update m i (x + y)) =
                  (fun m =>
                        mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                          (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                      (Function.update m i x) +
                    (fun m =>
                        mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                          (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                      (Function.update m i y)),
          map_smul' :=
            (_ :
              ∀ [inst : DecidableEq ι] (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
                (fun m =>
                      mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                        (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                    (Function.update m i (c • x)) =
                  c •
                    (fun m =>
                        mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                          (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                      (Function.update m i x)) }
        (max C 0)
        (_ :
          ∀ (m : (i : ι) → E i),
            ‖↑{
                      toFun := fun m =>
                        mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                          (_ : ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖),
                      map_add' :=
                        (_ :
                          ∀ [inst : DecidableEq ι] (m : (i : ι) → E i) (i : ι) (x y : E i),
                            (fun m =>
                                  mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                                    (_ :
                                      ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                                (Function.update m i (x + y)) =
                              (fun m =>
                                    mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                                      (_ :
                                        ∀ (m₂ : (i : ι') → E' i),
                                          ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                                  (Function.update m i x) +
                                (fun m =>
                                    mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                                      (_ :
                                        ∀ (m₂ : (i : ι') → E' i),
                                          ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                                  (Function.update m i y)),
                      map_smul' :=
                        (_ :
                          ∀ [inst : DecidableEq ι] (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
                            (fun m =>
                                  mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                                    (_ :
                                      ∀ (m₂ : (i : ι') → E' i), ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                                (Function.update m i (c • x)) =
                              c •
                                (fun m =>
                                    mkContinuous (↑f m) (C * ∏ i : ι, ‖m i‖)
                                      (_ :
                                        ∀ (m₂ : (i : ι') → E' i),
                                          ‖↑(↑f m) m₂‖ ≤ (C * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m₂ i‖))
                                  (Function.update m i x)) }
                  m‖ ≤
              max C 0 * ∏ i : ι, ‖m i‖)‖ ≤
    max C 0
exact mkContinuous_norm_le _ (le_max_right _ _) _