ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContDiffOn 𝕜 n f s ↔ (∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ∧ ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ<VAR>hf : DifferentiableOn 𝕜 f s<VAR>h : ContDiffOn 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f s ↔ ∃ f', ContDiffOn 𝕜 (↑n) f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ<VAR>hs : IsOpen s<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑n) (fun y => fderiv 𝕜 f y) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContDiffOn 𝕜 ⊤ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ⊤ (fun y => fderivWithin 𝕜 f s y) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>hs : IsOpen s<GOAL>ContDiffOn 𝕜 ⊤ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ⊤ (fun y => fderiv 𝕜 f y) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>m n : ℕ∞<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hmn : m + 1 ≤ n<GOAL>ContDiffOn 𝕜 m (fun y => fderivWithin 𝕜 f s y) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>m n : ℕ∞<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hs : IsOpen s<VAR>hmn : m + 1 ≤ n<GOAL>ContDiffOn 𝕜 m (fun y => fderiv 𝕜 f y) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>h : ContDiffOn 𝕜 n f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hn : 1 ≤ n<GOAL>ContinuousOn (fun x => fderivWithin 𝕜 f s x) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>h : ContDiffOn 𝕜 n f s<VAR>hs : IsOpen s<VAR>hn : 1 ≤ n<GOAL>ContinuousOn (fun x => fderiv 𝕜 f x) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>self : HasFTaylorSeriesUpTo n f p<VAR>x : E<GOAL>(p x 0).uncurry0 = f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>self : HasFTaylorSeriesUpTo n f p<VAR>m : ℕ<GOAL>↑m < n → ∀ (x : E), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>self : HasFTaylorSeriesUpTo n f p<VAR>m : ℕ<GOAL>↑m ≤ n → Continuous fun x => p x m
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpTo n f p<VAR>x : E<GOAL>p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>HasFTaylorSeriesUpToOn n f p Set.univ ↔ HasFTaylorSeriesUpTo n f p
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpTo n f p<VAR>s : Set E<GOAL>HasFTaylorSeriesUpToOn n f p s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpTo n f p<VAR>hmn : m ≤ n<GOAL>HasFTaylorSeriesUpTo m f p
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpTo n f p<GOAL>Continuous f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>HasFTaylorSeriesUpTo 0 f p ↔ Continuous f ∧ ∀ (x : E), (p x 0).uncurry0 = f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>HasFTaylorSeriesUpTo ⊤ f p ↔ ∀ (n : ℕ), HasFTaylorSeriesUpTo (↑n) f p
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>HasFTaylorSeriesUpTo ⊤ f p ↔ (∀ (x : E), (p x 0).uncurry0 = f x) ∧ ∀ (m : ℕ) (x : E), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpTo n f p<VAR>hn : 1 ≤ n<VAR>x : E<GOAL>HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpTo n f p<VAR>hn : 1 ≤ n<GOAL>Differentiable 𝕜 f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>HasFTaylorSeriesUpTo (↑(n + 1)) f p ↔ (∀ (x : E), (p x 0).uncurry0 = f x) ∧ (∀ (x : E), HasFDerivAt (fun y => p y 0) (p x 1).curryLeft x) ∧ HasFTaylorSeriesUpTo (↑n) (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) fun x => (p x).shift
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<GOAL>ContDiffWithinAt 𝕜 n f Set.univ x ↔ ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<GOAL>ContDiffAt 𝕜 ⊤ f x ↔ ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffAt 𝕜 n f x<GOAL>ContDiffWithinAt 𝕜 n f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hx : s ∈ 𝓝 x<GOAL>ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffOn 𝕜 n f s<VAR>hx : s ∈ 𝓝 x<GOAL>ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffAt 𝕜 n f x<VAR>hg : f₁ =ᶠ[𝓝 x] f<GOAL>ContDiffAt 𝕜 n f₁ x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>m n : ℕ∞<VAR>h : ContDiffAt 𝕜 n f x<VAR>hmn : m ≤ n<GOAL>ContDiffAt 𝕜 m f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffAt 𝕜 n f x<GOAL>ContinuousAt f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffAt 𝕜 n f x<VAR>hn : 1 ≤ n<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>m : ℕ<VAR>h : ContDiffAt 𝕜 n f x<VAR>hm : ↑m ≤ n<GOAL>∃ u ∈ 𝓝 x, ContDiffOn 𝕜 (↑m) f u
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ<GOAL>ContDiffAt 𝕜 (↑(n + 1)) f x ↔ ∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ<VAR>h : ContDiffAt 𝕜 (↑n) f x<GOAL>∀ᶠ (y : E) in 𝓝 x, ContDiffAt 𝕜 (↑n) f y
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>f' : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : HasFTaylorSeriesUpTo n f f'<GOAL>ContDiff 𝕜 n f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<GOAL>ContDiffOn 𝕜 n f Set.univ ↔ ContDiff 𝕜 n f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n f ↔ ∀ (x : E), ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiff 𝕜 n f<GOAL>ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiff 𝕜 n f<GOAL>ContDiffWithinAt 𝕜 n f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>ContDiff 𝕜 ⊤ f ↔ ∀ (n : ℕ), ContDiff 𝕜 (↑n) f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>(∀ (n : ℕ∞), ContDiff 𝕜 n f) ↔ ∀ (n : ℕ), ContDiff 𝕜 (↑n) f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>h : ContDiff 𝕜 n f<GOAL>ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>ContDiff 𝕜 0 f ↔ Continuous f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<GOAL>ContDiffAt 𝕜 0 f x ↔ ∃ u ∈ 𝓝 x, ContinuousOn f u
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<GOAL>ContDiffAt 𝕜 1 f x ↔ ∃ f', ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>m n : ℕ∞<VAR>h : ContDiff 𝕜 n f<VAR>hmn : m ≤ n<GOAL>ContDiff 𝕜 m f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ<VAR>h : ContDiff 𝕜 (↑n + 1) f<GOAL>ContDiff 𝕜 (↑n) f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ<VAR>h : ContDiff 𝕜 (↑n + 1) f<GOAL>ContDiff 𝕜 1 f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>h : ContDiff 𝕜 n f<GOAL>Continuous f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>h : ContDiff 𝕜 n f<VAR>hn : 1 ≤ n<GOAL>Differentiable 𝕜 f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n f ↔ ∀ (m : ℕ), ↑m ≤ n → ContDiff 𝕜 (↑m) f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ<GOAL>ContDiff 𝕜 (↑(n + 1)) f ↔ ∃ f', ContDiff 𝕜 (↑n) f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>ContDiff 𝕜 1 f ↔ ∃ f', Continuous f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>m : Fin 0 → E<GOAL>(iteratedFDeriv 𝕜 0 f x) m = f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>iteratedFDeriv 𝕜 0 f = ⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<GOAL>‖iteratedFDeriv 𝕜 0 f x‖ = ‖f x‖
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<GOAL>iteratedFDerivWithin 𝕜 0 f s = iteratedFDeriv 𝕜 0 f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ<VAR>m : Fin (n + 1) → E<GOAL>(iteratedFDeriv 𝕜 (n + 1) f x) m = ((fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) (m 0)) (Fin.tail m)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ<GOAL>iteratedFDeriv 𝕜 (n + 1) f = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ<GOAL>fderiv 𝕜 (iteratedFDeriv 𝕜 n f) = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ iteratedFDeriv 𝕜 (n + 1) f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ<GOAL>tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ<GOAL>Function.support (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>hf : HasCompactSupport f<VAR>n : ℕ<GOAL>HasCompactSupport (iteratedFDeriv 𝕜 n f)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ<GOAL>‖fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ<GOAL>iteratedFDerivWithin 𝕜 n f Set.univ = iteratedFDeriv 𝕜 n f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpTo n f p<VAR>m : ℕ<VAR>hmn : ↑m ≤ n<VAR>x : E<GOAL>p x m = iteratedFDeriv 𝕜 m f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ<VAR>hs : IsOpen s<GOAL>Set.EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>ftaylorSeriesWithin 𝕜 f Set.univ = ftaylorSeries 𝕜 f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ<VAR>m : Fin (n + 1) → E<GOAL>(iteratedFDeriv 𝕜 (n + 1) f x) m = ((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) (Fin.init m)) (m (Fin.last n))
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ<GOAL>iteratedFDeriv 𝕜 (n + 1) f x = (⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F) ∘ iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ<GOAL>‖iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>m : Fin 1 → E<GOAL>(iteratedFDeriv 𝕜 1 f x) m = (fderiv 𝕜 f x) (m 0)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>z : E<VAR>m : Fin 2 → E<GOAL>(iteratedFDeriv 𝕜 2 f z) m = ((fderiv 𝕜 (fderiv 𝕜 f) z) (m 0)) (m 1)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n f ↔ HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n f ↔ (∀ (m : ℕ), ↑m ≤ n → Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧ ∀ (m : ℕ), ↑m < n → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>hf : ContDiff 𝕜 n f<GOAL>Continuous fun x => iteratedFDeriv 𝕜 m f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>m : ℕ<VAR>hm : ↑m < n<VAR>hf : ContDiff 𝕜 n f<GOAL>Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>h : ∀ (m : ℕ), ↑m ≤ n → Differentiable 𝕜 (iteratedFDeriv 𝕜 m f)<GOAL>ContDiff 𝕜 n f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ<GOAL>ContDiff 𝕜 (↑(n + 1)) f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 ↑n fun y => fderiv 𝕜 f y
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>ContDiff 𝕜 1 f ↔ Differentiable 𝕜 f ∧ Continuous (fderiv 𝕜 f)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>ContDiff 𝕜 ⊤ f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 ⊤ fun y => fderiv 𝕜 f y