Theorem: ContinuousLinearMap.continuous_pi (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)
f : (i : ι) → X → M →L[𝕜] φ i
hf : ∀ (i : ι), Continuous fun x => f i x
⊢ Continuous fun x => pi fun i => f i x
Tactic:
simp only [← piL_apply]
State after:
𝕜 : 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)
f : (i : ι) → X → M →L[𝕜] φ i
hf : ∀ (i : ι), Continuous fun x => f i x
⊢ Continuous fun x => (piL 𝕜 M fun i => φ i) fun i => f i x

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)
f : (i : ι) → X → M →L[𝕜] φ i
hf : ∀ (i : ι), Continuous fun x => f i x
⊢ Continuous fun x => (piL 𝕜 M fun i => φ i) fun i => f i x
Tactic:
refine .clm_apply continuous_const (_root_.continuous_pi hf)
State after:
no goals