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>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>HasFTaylorSeriesUpToOn (↑(n + 1)) f p s ↔ (∀ x ∈ s, (p x 0).uncurry0 = f x) ∧ (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧ HasFTaylorSeriesUpToOn (↑n) (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) 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>x : E<VAR>n : ℕ<GOAL>ContDiffWithinAt 𝕜 (↑n) f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑n) f p 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>s : Set E<VAR>f : E → F<VAR>x : E<VAR>m n : ℕ∞<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hmn : m ≤ n<GOAL>ContDiffWithinAt 𝕜 m 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 : ℕ∞<GOAL>ContDiffWithinAt 𝕜 n f s x ↔ ∀ (m : ℕ), ↑m ≤ n → ContDiffWithinAt 𝕜 (↑m) 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<GOAL>ContDiffWithinAt 𝕜 ⊤ f s x ↔ ∀ (n : ℕ), 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<GOAL>ContinuousWithinAt 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 f₁ : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = 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 f₁ : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>h₁ : f₁ =ᶠ[𝓝[insert x s] x] 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>s : Set E<VAR>f f₁ : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : x ∈ s<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 f₁ : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>ContDiffWithinAt 𝕜 n f₁ s x ↔ 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 f₁ : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>h₁ : ∀ y ∈ s, f₁ y = f y<VAR>hx : f₁ x = 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 f₁ : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>h₁ : ∀ y ∈ s, f₁ y = f y<VAR>hx : x ∈ s<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>t : Set E<VAR>hst : s ∈ 𝓝[t] x<GOAL>ContDiffWithinAt 𝕜 n f t 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>t : Set E<VAR>hst : t ⊆ s<GOAL>ContDiffWithinAt 𝕜 n f t 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>t : Set E<VAR>hst : 𝓝[s] x = 𝓝[t] x<GOAL>ContDiffWithinAt 𝕜 n f t 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>t : Set E<VAR>hst : 𝓝[s] x = 𝓝[t] x<GOAL>ContDiffWithinAt 𝕜 n f s x ↔ ContDiffWithinAt 𝕜 n f t 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 t : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : t ∈ 𝓝[s] x<GOAL>ContDiffWithinAt 𝕜 n f (s ∩ t) x ↔ 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 t : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : t ∈ 𝓝 x<GOAL>ContDiffWithinAt 𝕜 n f (s ∩ t) x ↔ 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 : ℕ∞<GOAL>ContDiffWithinAt 𝕜 n f (insert x s) x ↔ 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>y : E<GOAL>ContDiffWithinAt 𝕜 n f (insert y s) x ↔ 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<GOAL>ContDiffWithinAt 𝕜 n f (insert 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>x : E<VAR>n : ℕ∞<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hn : 1 ≤ n<GOAL>DifferentiableWithinAt 𝕜 f (insert 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>x : E<VAR>n : ℕ∞<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hn : 1 ≤ n<GOAL>DifferentiableWithinAt 𝕜 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 : ℕ<GOAL>ContDiffWithinAt 𝕜 (↑(n + 1)) f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n) f' u 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 : ℕ<GOAL>ContDiffWithinAt 𝕜 (↑(n + 1)) f s x ↔ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ 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>n : ℕ∞<VAR>f' : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : HasFTaylorSeriesUpToOn n f f' s<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>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffOn 𝕜 n f s<VAR>hx : x ∈ s<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>m : ℕ<VAR>hm : ↑m ≤ n<VAR>h : ContDiffWithinAt 𝕜 n f s x<GOAL>∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m) f (insert x s ∩ 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>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>h : ContDiffWithinAt 𝕜 n f s x<GOAL>∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ 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>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ<VAR>h : ContDiffWithinAt 𝕜 (↑n) f s x<GOAL>∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑n) f s 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>s : Set E<VAR>f : E → F<VAR>m n : ℕ∞<VAR>h : ContDiffOn 𝕜 n f s<VAR>hmn : m ≤ n<GOAL>ContDiffOn 𝕜 m 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>h : ContDiffOn 𝕜 (↑n + 1) f s<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>s : Set E<VAR>f : E → F<VAR>n : ℕ<VAR>h : ContDiffOn 𝕜 (↑n + 1) f s<GOAL>ContDiffOn 𝕜 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 : ℕ∞<GOAL>ContDiffOn 𝕜 n f s ↔ ∀ (m : ℕ), ↑m ≤ n → ContDiffOn 𝕜 (↑m) 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<GOAL>ContDiffOn 𝕜 ⊤ f s ↔ ∀ (n : ℕ), 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>s : Set E<VAR>f : E → F<GOAL>(∀ (n : ℕ∞), ContDiffOn 𝕜 n f s) ↔ ∀ (n : ℕ), 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>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>h : ContDiffOn 𝕜 n f s<GOAL>ContinuousOn 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 f₁ : E → F<VAR>n : ℕ∞<VAR>h : ContDiffOn 𝕜 n f s<VAR>h₁ : ∀ x ∈ s, f₁ x = f x<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>s : Set E<VAR>f f₁ : E → F<VAR>n : ℕ∞<VAR>h₁ : ∀ x ∈ s, f₁ x = f x<GOAL>ContDiffOn 𝕜 n f₁ s ↔ 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>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>h : ContDiffOn 𝕜 n f s<VAR>t : Set E<VAR>hst : t ⊆ s<GOAL>ContDiffOn 𝕜 n f t
<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 s₁ : Set E<VAR>f f₁ : E → F<VAR>n : ℕ∞<VAR>hf : ContDiffOn 𝕜 n f s<VAR>h₁ : ∀ x ∈ s₁, f₁ x = f x<VAR>hs : s₁ ⊆ s<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>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>h : ContDiffOn 𝕜 n f s<VAR>hn : 1 ≤ n<GOAL>DifferentiableOn 𝕜 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>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)<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>s : Set E<VAR>f : E → F<VAR>n : ℕ<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f s ↔ ∀ x ∈ s, ∃ u ∈ 𝓝[insert x s] x, ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 (↑n) 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>s : Set E<VAR>f : E → F<VAR>x : E<VAR>m : Fin 0 → E<GOAL>(iteratedFDerivWithin 𝕜 0 f s 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>s : Set E<VAR>f : E → F<GOAL>iteratedFDerivWithin 𝕜 0 f s = ⇑(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>s : Set E<VAR>f : E → F<VAR>x : E<GOAL>‖iteratedFDerivWithin 𝕜 0 f s 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<VAR>x : E<VAR>n : ℕ<VAR>m : Fin (n + 1) → E<GOAL>(iteratedFDerivWithin 𝕜 (n + 1) f s x) m = ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s 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>s : Set E<VAR>f : E → F<VAR>n : ℕ<GOAL>iteratedFDerivWithin 𝕜 (n + 1) f s = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) 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>s : Set E<VAR>n : ℕ<GOAL>fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ iteratedFDerivWithin 𝕜 (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>x : E<VAR>n : ℕ<GOAL>‖fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) 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>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>m : Fin (n + 1) → E<GOAL>(iteratedFDerivWithin 𝕜 (n + 1) f s x) m = ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s 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>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>iteratedFDerivWithin 𝕜 (n + 1) f s x = (⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F) ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) 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>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>‖iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) 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>h : UniqueDiffWithinAt 𝕜 s x<VAR>m : Fin 1 → E<GOAL>(iteratedFDerivWithin 𝕜 1 f s x) m = (fderivWithin 𝕜 f s 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>s : Set E<VAR>f : E → F<VAR>z : E<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hz : z ∈ s<VAR>m : Fin 2 → E<GOAL>(iteratedFDerivWithin 𝕜 2 f s z) m = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s 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>s t : Set E<VAR>f f₁ : E → F<VAR>x : E<VAR>h : f₁ =ᶠ[𝓝[s] x] f<VAR>ht : t ⊆ s<VAR>n : ℕ<GOAL>iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t
<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 f₁ : E → F<VAR>x : E<VAR>h : f₁ =ᶠ[𝓝[s] x] f<VAR>n : ℕ<GOAL>iteratedFDerivWithin 𝕜 n f₁ s =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 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>s : Set E<VAR>f f₁ : E → F<VAR>x : E<VAR>h : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<VAR>n : ℕ<GOAL>iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 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 f₁ : E → F<VAR>x : E<VAR>hs : Set.EqOn f₁ f s<VAR>hx : x ∈ s<VAR>n : ℕ<GOAL>iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 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 f₁ : E → F<VAR>hs : Set.EqOn f₁ f s<VAR>n : ℕ<GOAL>Set.EqOn (iteratedFDerivWithin 𝕜 n f₁ s) (iteratedFDerivWithin 𝕜 n f s) 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 t : Set E<VAR>f : E → F<VAR>x : E<VAR>y : E<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<VAR>n : ℕ<GOAL>iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t
<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 t : Set E<VAR>f : E → F<VAR>x : E<VAR>h : s =ᶠ[𝓝 x] t<VAR>n : ℕ<GOAL>iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t
<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 t : Set E<VAR>f : E → F<VAR>x : E<VAR>h : s =ᶠ[𝓝 x] t<VAR>n : ℕ<GOAL>iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t 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 u : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ<VAR>hu : u ∈ 𝓝[s] x<GOAL>iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 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 u : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ<VAR>hu : u ∈ 𝓝 x<GOAL>iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 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 u : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ<VAR>hu : IsOpen u<VAR>hx : x ∈ u<GOAL>iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 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<GOAL>ContDiffOn 𝕜 0 f s ↔ ContinuousOn 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>x : E<VAR>hx : x ∈ s<GOAL>ContDiffWithinAt 𝕜 0 f s x ↔ ∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ 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>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>m : ℕ<VAR>hmn : ↑m ≤ n<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>p x m = iteratedFDerivWithin 𝕜 m 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>n : ℕ∞<VAR>h : ContDiffOn 𝕜 n f s<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) 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>Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s<VAR>Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s<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>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>h : ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s<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>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>m : ℕ<VAR>h : ContDiffOn 𝕜 n f s<VAR>hmn : ↑m ≤ n<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContinuousOn (iteratedFDerivWithin 𝕜 m f s) 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>m : ℕ<VAR>h : ContDiffOn 𝕜 n f s<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) 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>x : E<VAR>n : ℕ∞<VAR>m : ℕ<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 (insert x s)<GOAL>DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x