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

State before:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝¹⁴ : Fintype ι
inst✝¹³ : DecidableEq ι
X : Type u_3
inst✝¹² : TopologicalSpace X
D : ι → Type u_4
inst✝¹¹ : (i : ι) → NormedAddCommGroup (D i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (D i)
D₁ : ι → Type u_5
inst✝⁹ : (i : ι) → NormedAddCommGroup (D₁ i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (D₁ i)
E : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
E₁ : Type u_7
inst✝⁵ : NormedAddCommGroup E₁
inst✝⁴ : NormedSpace 𝕜 E₁
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_9
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → X → E →L[𝕜] F
hf : ∀ (i : ι), Continuous fun x => f i x
⊢ Continuous fun x => piMap fun i => f i x
Tactic:
simp only [← piMapL_apply]
State after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝¹⁴ : Fintype ι
inst✝¹³ : DecidableEq ι
X : Type u_3
inst✝¹² : TopologicalSpace X
D : ι → Type u_4
inst✝¹¹ : (i : ι) → NormedAddCommGroup (D i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (D i)
D₁ : ι → Type u_5
inst✝⁹ : (i : ι) → NormedAddCommGroup (D₁ i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (D₁ i)
E : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
E₁ : Type u_7
inst✝⁵ : NormedAddCommGroup E₁
inst✝⁴ : NormedSpace 𝕜 E₁
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_9
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → X → E →L[𝕜] F
hf : ∀ (i : ι), Continuous fun x => f i x
⊢ Continuous fun x => (piMapL 𝕜 (fun i => E) fun i => F) fun i => f i x

State before:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝¹⁴ : Fintype ι
inst✝¹³ : DecidableEq ι
X : Type u_3
inst✝¹² : TopologicalSpace X
D : ι → Type u_4
inst✝¹¹ : (i : ι) → NormedAddCommGroup (D i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (D i)
D₁ : ι → Type u_5
inst✝⁹ : (i : ι) → NormedAddCommGroup (D₁ i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (D₁ i)
E : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
E₁ : Type u_7
inst✝⁵ : NormedAddCommGroup E₁
inst✝⁴ : NormedSpace 𝕜 E₁
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_9
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → X → E →L[𝕜] F
hf : ∀ (i : ι), Continuous fun x => f i x
⊢ Continuous fun x => (piMapL 𝕜 (fun i => E) fun i => F) fun i => f i x
Tactic:
exact .clm_apply continuous_const (_root_.continuous_pi hf)
State after:
no goals