𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : ℕ∞
f : V →A[𝕜] W
⊢ ContDiff 𝕜 n (↑(contLinear f) + Function.const V (↑f 0))
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : ℕ∞
f : V →A[𝕜] W
⊢ ContDiff 𝕜 n ↑f
rw [f.decomp]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : ℕ∞
f : V →A[𝕜] W
⊢ ContDiff 𝕜 n fun x => Function.const V (↑f 0) x
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : ℕ∞
f : V →A[𝕜] W
⊢ ContDiff 𝕜 n (↑(contLinear f) + Function.const V (↑f 0))
apply f.contLinear.contDiff.add
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : ℕ∞
f : V →A[𝕜] W
⊢ ContDiff 𝕜 n fun x => Function.const V (↑f 0) x
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : ℕ∞
f : V →A[𝕜] W
⊢ ContDiff 𝕜 n fun x => Function.const V (↑f 0) x
simp only
no goals
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : ℕ∞
f : V →A[𝕜] W
⊢ ContDiff 𝕜 n fun x => Function.const V (↑f 0) x
exact contDiff_const