case Hcont
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.34703
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s

case Hdiff
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.34703
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.34703
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ContDiffOn 𝕜 n f s
apply contDiffOn_of_continuousOn_differentiableOn
no goals
case Hcont
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.34703
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s
simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_continuousOn_iff]
no goals
case Hdiff
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.34703
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s
simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_iff]