Theorem: ContinuousLinearMap.pi_eq_sum_single_proj (ForML/ContinuousLinearMap.lean)

State before:
𝕜 : Type u_1
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
X : Type u_3
inst✝⁵ : TopologicalSpace X
M : Type u_4
inst✝⁴ : NormedAddCommGroup M
φ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (φ i)
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 M
inst✝ : (i : ι) → NormedSpace 𝕜 (φ i)
⊢ pi = ⇑(∑ i : ι, comp ((compL 𝕜 M (φ i) ((i : ι) → φ i)) (single i)) (proj i))
Tactic:
ext
State after:
case h.h.h
𝕜 : Type u_1
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
X : Type u_3
inst✝⁵ : TopologicalSpace X
M : Type u_4
inst✝⁴ : NormedAddCommGroup M
φ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (φ i)
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 M
inst✝ : (i : ι) → NormedSpace 𝕜 (φ i)
x✝² : (i : ι) → M →L[𝕜] φ i
x✝¹ : M
x✝ : ι
⊢ (pi x✝²) x✝¹ x✝ = ((∑ i : ι, comp ((compL 𝕜 M (φ i) ((i : ι) → φ i)) (single i)) (proj i)) x✝²) x✝¹ x✝

State before:
case h.h.h
𝕜 : Type u_1
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
X : Type u_3
inst✝⁵ : TopologicalSpace X
M : Type u_4
inst✝⁴ : NormedAddCommGroup M
φ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (φ i)
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 M
inst✝ : (i : ι) → NormedSpace 𝕜 (φ i)
x✝² : (i : ι) → M →L[𝕜] φ i
x✝¹ : M
x✝ : ι
⊢ (pi x✝²) x✝¹ x✝ = ((∑ i : ι, comp ((compL 𝕜 M (φ i) ((i : ι) → φ i)) (single i)) (proj i)) x✝²) x✝¹ x✝
Tactic:
simp
State after:
no goals