internlm/Lean-Github huggingface dataset:
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
i : ι
⊢ HasFDerivAt (fun f => (f i) (x i))
    (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i)) f
Tactic:
simp only [← ContinuousLinearMap.proj_apply (R := 𝕜) (φ := fun i ↦ E i →L[𝕜] E₁ i) i]
Proof state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
i : ι
⊢ HasFDerivAt (fun f => ((ContinuousLinearMap.proj i) f) (x i))
    (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i)) f
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
i : ι
⊢ HasFDerivAt (fun f => ((ContinuousLinearMap.proj i) f) (x i))
    (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i)) f
Tactic:
simp only [← ContinuousLinearMap.apply_apply (x i)]
Proof state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
i : ι
⊢ HasFDerivAt (fun f => ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) ((ContinuousLinearMap.proj i) f))
    (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i)) f
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
i : ι
⊢ HasFDerivAt (fun f => ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) ((ContinuousLinearMap.proj i) f))
    (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i)) f
Tactic:
simp only [← ContinuousLinearMap.comp_apply]
Proof state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
i : ι
⊢ HasFDerivAt
    (fun f => (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i)) f)
    (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i)) f
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
i : ι
⊢ HasFDerivAt
    (fun f => (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i)) f)
    (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i)) f
Tactic:
exact ContinuousLinearMap.hasFDerivAt _
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H.refine_1
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
i : ι
a✝ : i ∈ Finset.univ
⊢ (df i) (x i) = (Function.update f i (df i) i) (x i)
Tactic:
simp
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H.refine_2
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
i : ι
a✝ : i ∈ Finset.univ
⊢ ∀ (x_1 : ι), x_1 ≠ i → (f x_1) (x x_1) = (Function.update f i (df i) x_1) (x x_1)
Tactic:
intro j hji
Proof state after:
case H.refine_2
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
i : ι
a✝ : i ∈ Finset.univ
j : ι
hji : j ≠ i
⊢ (f j) (x j) = (Function.update f i (df i) j) (x j)
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H.refine_2
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
i : ι
a✝ : i ∈ Finset.univ
j : ι
hji : j ≠ i
⊢ (f j) (x j) = (Function.update f i (df i) j) (x j)
Tactic:
simp [hji]
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.clm_update_apply
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
x : (i : ι) → E i
⊢ (fun i => (Function.update f j b i) (x i)) = Function.update (fun i => (f i) (x i)) j (b (x j))
Tactic:
rw [Function.eq_update_iff]
Proof state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
x : (i : ι) → E i
⊢ (Function.update f j b j) (x j) = b (x j) ∧
    ∀ (x_1 : ι), x_1 ≠ j → (Function.update f j b x_1) (x x_1) = (f x_1) (x x_1)
Theorem: ContinuousMultilinearMap.clm_update_apply
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
x : (i : ι) → E i
⊢ (Function.update f j b j) (x j) = b (x j) ∧
    ∀ (x_1 : ι), x_1 ≠ j → (Function.update f j b x_1) (x x_1) = (f x_1) (x x_1)
Tactic:
refine And.intro ?_ ?_
Proof state after:
case refine_1
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
x : (i : ι) → E i
⊢ (Function.update f j b j) (x j) = b (x j)

case refine_2
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
x : (i : ι) → E i
⊢ ∀ (x_1 : ι), x_1 ≠ j → (Function.update f j b x_1) (x x_1) = (f x_1) (x x_1)
Theorem: ContinuousMultilinearMap.clm_update_apply
Proof state before:
case refine_1
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
x : (i : ι) → E i
⊢ (Function.update f j b j) (x j) = b (x j)
Tactic:
simp
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.clm_update_apply
Proof state before:
case refine_2
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
x : (i : ι) → E i
⊢ ∀ (x_1 : ι), x_1 ≠ j → (Function.update f j b x_1) (x x_1) = (f x_1) (x x_1)
Tactic:
intro i h
Proof state after:
case refine_2
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
x : (i : ι) → E i
i : ι
h : i ≠ j
⊢ (Function.update f j b i) (x i) = (f i) (x i)
Theorem: ContinuousMultilinearMap.clm_update_apply
Proof state before:
case refine_2
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
x : (i : ι) → E i
i : ι
h : i ≠ j
⊢ (Function.update f j b i) (x i) = (f i) (x i)
Tactic:
simp [h]
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.compContinuousLinearMap_update
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
q : (E j →L[𝕜] E₁ j) →L[𝕜] ContinuousMultilinearMap 𝕜 E G
⊢ compContinuousLinearMap g (Function.update f j b) = q b
Tactic:
refine ContinuousMultilinearMap.ext ?_
Proof state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
q : (E j →L[𝕜] E₁ j) →L[𝕜] ContinuousMultilinearMap 𝕜 E G
⊢ ∀ (x : (i : ι) → E i), (compContinuousLinearMap g (Function.update f j b)) x = (q b) x
Theorem: ContinuousMultilinearMap.compContinuousLinearMap_update
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
q : (E j →L[𝕜] E₁ j) →L[𝕜] ContinuousMultilinearMap 𝕜 E G
⊢ ∀ (x : (i : ι) → E i), (compContinuousLinearMap g (Function.update f j b)) x = (q b) x
Tactic:
intro x
Proof state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
q : (E j →L[𝕜] E₁ j) →L[𝕜] ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ (compContinuousLinearMap g (Function.update f j b)) x = (q b) x