ext x
ι : Type u_1
𝕜 : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
g : ContinuousMultilinearMap 𝕜 M₁ F
⊢ (continuousMultilinearCurryLeftEquiv 𝕜 M₁ F) (ContinuousMultilinearMap.curryLeft g) = g
case H
ι : Type u_1
𝕜 : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
g : ContinuousMultilinearMap 𝕜 M₁ F
x : (i : Fin (Nat.succ n)) → M₁ i
⊢ ((continuousMultilinearCurryLeftEquiv 𝕜 M₁ F) (ContinuousMultilinearMap.curryLeft g)) x = g x