ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>f : E →SL[σ] F<GOAL>Function.Bijective ⇑f ↔ (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>f : E →SL[σ] F<VAR>c : ℝ≥0<VAR>hf : AntilipschitzWith c ⇑f<GOAL>CompleteSpace ↥(LinearMap.range f)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>f' : 𝕜 →L[𝕜] F<GOAL>HasFDerivAtFilter f f' x L ↔ HasDerivAtFilter f (f' 1) x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>f' : 𝕜 →L[𝕜] F<GOAL>HasFDerivAtFilter f f' x L → HasDerivAtFilter f (f' 1) x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>f' : 𝕜 →L[𝕜] F<GOAL>HasFDerivWithinAt f f' s x ↔ HasDerivWithinAt f (f' 1) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>f' : F<GOAL>HasDerivWithinAt f f' s x ↔ HasFDerivWithinAt f (ContinuousLinearMap.smulRight 1 f') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>f' : 𝕜 →L[𝕜] F<GOAL>HasFDerivWithinAt f f' s x → HasDerivWithinAt f (f' 1) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>f' : F<GOAL>HasDerivWithinAt f f' s x → HasFDerivWithinAt f (ContinuousLinearMap.smulRight 1 f') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>f' : 𝕜 →L[𝕜] F<GOAL>HasFDerivAt f f' x ↔ HasDerivAt f (f' 1) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>f' : 𝕜 →L[𝕜] F<GOAL>HasFDerivAt f f' x → HasDerivAt f (f' 1) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>f' : 𝕜 →L[𝕜] F<GOAL>HasStrictFDerivAt f f' x ↔ HasStrictDerivAt f (f' 1) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>f' : 𝕜 →L[𝕜] F<GOAL>HasStrictFDerivAt f f' x → HasStrictDerivAt f (f' 1) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<GOAL>HasStrictDerivAt f f' x ↔ HasStrictFDerivAt f (ContinuousLinearMap.smulRight 1 f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>f' : F<GOAL>HasDerivAt f f' x ↔ HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : ¬DifferentiableWithinAt 𝕜 f s x<GOAL>derivWithin f s x = 0
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : 𝓝[s \ {x}] x = ⊥<GOAL>derivWithin f s x = 0
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : x ∉ closure s<GOAL>derivWithin f s x = 0
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : derivWithin f s x ≠ 0<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>h : ¬DifferentiableAt 𝕜 f x<GOAL>deriv f x = 0
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>h : deriv f x ≠ 0<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' f₁' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>H : UniqueDiffWithinAt 𝕜 s x<VAR>h : HasDerivWithinAt f f' s x<VAR>h₁ : HasDerivWithinAt f f₁' s x<GOAL>f' = f₁'
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<GOAL>HasDerivAtFilter f f' x L ↔ (fun x' => f x' - f x - (x' - x) • f') =o[L] fun x' => x' - x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<GOAL>HasDerivAtFilter f f' x L ↔ Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - (x' - x) • f'‖) L (𝓝 0)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>HasDerivWithinAt f f' s x ↔ (fun x' => f x' - f x - (x' - x) • f') =o[𝓝[s] x] fun x' => x' - x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>HasDerivWithinAt f f' s x ↔ Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - (x' - x) • f'‖) (𝓝[s] x) (𝓝 0)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<GOAL>HasDerivAt f f' x ↔ (fun x' => f x' - f x - (x' - x) • f') =o[𝓝 x] fun x' => x' - x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<GOAL>HasDerivAt f f' x ↔ Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - (x' - x) • f'‖) (𝓝 x) (𝓝 0)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>h : HasDerivAtFilter f f' x L<GOAL>(fun x' => f x' - f x) =O[L] fun x' => x' - x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>hf : HasDerivAtFilter f f' x L<VAR>hf' : f' ≠ 0<GOAL>(fun x' => x' - x) =O[L] fun x' => f x' - f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>h : HasStrictDerivAt f f' x<GOAL>HasDerivAt f f' x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>y : 𝕜<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<GOAL>HasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>h : s =ᶠ[𝓝 x] t<GOAL>HasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>HasDerivWithinAt f f' (s \ {x}) x ↔ HasDerivWithinAt f f' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>PartialOrder 𝕜<GOAL>HasDerivWithinAt f f' (Set.Ioi x) x ↔ HasDerivWithinAt f f' (Set.Ici x) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>PartialOrder 𝕜<GOAL>HasDerivWithinAt f f' (Set.Iio x) x ↔ HasDerivWithinAt f f' (Set.Iic x) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>LinearOrder 𝕜<VAR>OrderClosedTopology 𝕜<VAR>x y : 𝕜<VAR>h : x < y<GOAL>HasDerivWithinAt f f' (Set.Ioo x y) x ↔ HasDerivWithinAt f f' (Set.Ioi x) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<GOAL>HasDerivAt f f' x ↔ (fun h => f (x + h) - f x - h • f') =o[𝓝 0] fun h => h
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>L₁ L₂ : Filter 𝕜<VAR>h : HasDerivAtFilter f f' x L₂<VAR>hst : L₁ ≤ L₂<GOAL>HasDerivAtFilter f f' x L₁
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>h : HasDerivWithinAt f f' t x<VAR>hst : s ⊆ t<GOAL>HasDerivWithinAt f f' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>h : HasDerivWithinAt f f' t x<VAR>hst : t ∈ 𝓝[s] x<GOAL>HasDerivWithinAt f f' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>h : HasDerivAt f f' x<VAR>hL : L ≤ 𝓝 x<GOAL>HasDerivAtFilter f f' x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : HasDerivAt f f' x<GOAL>HasDerivWithinAt f f' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : HasDerivWithinAt f f' s x<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>h : HasDerivAt f f' x<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<GOAL>HasDerivWithinAt f f' Set.univ x ↔ HasDerivAt f f' x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f₀' f₁' : F<VAR>x : 𝕜<VAR>h₀ : HasDerivAt f f₀' x<VAR>h₁ : HasDerivAt f f₁' x<GOAL>f₀' = f₁'
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>h : t ∈ 𝓝[s] x<GOAL>HasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>h : t ∈ 𝓝 x<GOAL>HasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>hs : HasDerivWithinAt f f' s x<VAR>ht : HasDerivWithinAt f f' t x<GOAL>HasDerivWithinAt f f' (s ∪ t) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : HasDerivWithinAt f f' s x<VAR>hs : s ∈ 𝓝 x<GOAL>HasDerivAt f f' x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : DifferentiableWithinAt 𝕜 f s x<GOAL>HasDerivWithinAt f (derivWithin f s x) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>h : DifferentiableAt 𝕜 f x<GOAL>HasDerivAt f (deriv f x) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<GOAL>HasDerivAt f (deriv f x) x ↔ DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>HasDerivWithinAt f (derivWithin f s x) s x ↔ DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : DifferentiableOn 𝕜 f s<VAR>hs : s ∈ 𝓝 x<GOAL>HasDerivAt f (deriv f x) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>h : HasDerivAt f f' x<GOAL>deriv f x = f'
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f' : 𝕜 → F<VAR>h : ∀ (x : 𝕜), HasDerivAt f (f' x) x<GOAL>deriv f = f'
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : HasDerivWithinAt f f' s x<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin f s x = f'
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>(fderivWithin 𝕜 f s x) 1 = derivWithin f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>ContinuousLinearMap.smulRight 1 (derivWithin f s x) = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>‖derivWithin f s x‖ = ‖fderivWithin 𝕜 f s x‖
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<GOAL>(fderiv 𝕜 f x) 1 = deriv f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>y : 𝕜<GOAL>(fderiv 𝕜 f x) y = y • deriv f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<GOAL>ContinuousLinearMap.smulRight 1 (deriv f x) = fderiv 𝕜 f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>f : 𝕜 → 𝕜<VAR>x y : 𝕜<GOAL>(fderiv 𝕜 f x) y = deriv f x * y
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<GOAL>‖deriv f x‖ = ‖fderiv 𝕜 f x‖
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : DifferentiableAt 𝕜 f x<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin f s x = deriv f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hd : HasDerivWithinAt f 0 s x<VAR>H : UniqueDiffWithinAt 𝕜 s x<GOAL>deriv f x = 0
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>st : t ∈ 𝓝[s] x<VAR>ht : UniqueDiffWithinAt 𝕜 s x<VAR>h : DifferentiableWithinAt 𝕜 f t x<GOAL>derivWithin f s x = derivWithin f t x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>st : s ⊆ t<VAR>ht : UniqueDiffWithinAt 𝕜 s x<VAR>h : DifferentiableWithinAt 𝕜 f t x<GOAL>derivWithin f s x = derivWithin f t x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>y : 𝕜<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<GOAL>derivWithin f s x = derivWithin f t x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>h : s =ᶠ[𝓝 x] t<GOAL>derivWithin f s x = derivWithin f t x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<GOAL>derivWithin f Set.univ = deriv f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>ht : t ∈ 𝓝 x<GOAL>derivWithin f (s ∩ t) x = derivWithin f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : s ∈ 𝓝 x<GOAL>derivWithin f s x = deriv f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hs : IsOpen s<VAR>hx : x ∈ s<GOAL>derivWithin f s x = deriv f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>f' : 𝕜 → F<VAR>hs : IsOpen s<VAR>hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<GOAL>Set.EqOn (deriv f) f' s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set F<VAR>x : 𝕜<GOAL>deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>t : Set 𝕜<VAR>s : Set F<VAR>x : 𝕜<GOAL>derivWithin f t x ∈ s ↔ DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>PartialOrder 𝕜<GOAL>DifferentiableWithinAt 𝕜 f (Set.Ioi x) x ↔ DifferentiableWithinAt 𝕜 f (Set.Ici x) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x : ℝ<GOAL>derivWithin f (Set.Ioi x) x = derivWithin f (Set.Ici x) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₀ f₁ : 𝕜 → F<VAR>f₀' f₁' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>h₀ : f₀ =ᶠ[L] f₁<VAR>hx : f₀ x = f₁ x<VAR>h₁ : f₀' = f₁'<GOAL>HasDerivAtFilter f₀ f₀' x L ↔ HasDerivAtFilter f₁ f₁' x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>h : HasDerivAtFilter f f' x L<VAR>hL : f₁ =ᶠ[L] f<VAR>hx : f₁ x = f x<GOAL>HasDerivAtFilter f₁ f' x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>h : HasDerivWithinAt f f' s x<VAR>ht : ∀ x ∈ t, f₁ x = f x<VAR>hx : f₁ x = f x<VAR>h₁ : t ⊆ s<GOAL>HasDerivWithinAt f₁ f' t x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : HasDerivWithinAt f f' s x<VAR>hs : ∀ x ∈ s, f₁ x = f x<VAR>hx : f₁ x = f x<GOAL>HasDerivWithinAt f₁ f' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : HasDerivWithinAt f f' s x<VAR>hs : ∀ x ∈ s, f₁ x = f x<VAR>hx : x ∈ s<GOAL>HasDerivWithinAt f₁ f' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : HasDerivWithinAt f f' s x<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>HasDerivWithinAt f₁ f' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>HasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : HasDerivWithinAt f f' s x<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : x ∈ s<GOAL>HasDerivWithinAt f₁ f' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : x ∈ s<GOAL>HasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' g' : F<VAR>x : 𝕜<VAR>h : HasStrictDerivAt f f' x<VAR>h' : f' = g'<GOAL>HasStrictDerivAt f g' x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' g' : F<VAR>x : 𝕜<VAR>h : HasDerivAt f f' x<VAR>h' : f' = g'<GOAL>HasDerivAt f g' x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' g' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>h : HasDerivWithinAt f f' s x<VAR>h' : f' = g'<GOAL>HasDerivWithinAt f g' s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>h : HasDerivAt f f' x<VAR>h₁ : f₁ =ᶠ[𝓝 x] f<GOAL>HasDerivAt f₁ f' x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₀ f₁ : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>h : f₀ =ᶠ[𝓝 x] f₁<GOAL>HasDerivAt f₀ f' x ↔ HasDerivAt f₁ f' x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hs : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>derivWithin f₁ s x = derivWithin f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hs : Set.EqOn f₁ f s<VAR>hx : f₁ x = f x<GOAL>derivWithin f₁ s x = derivWithin f s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>x : 𝕜<VAR>hL : f₁ =ᶠ[𝓝 x] f<GOAL>deriv f₁ x = deriv f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : 𝕜 → F<VAR>x : 𝕜<VAR>h : f₁ =ᶠ[𝓝 x] f<GOAL>deriv f₁ =ᶠ[𝓝 x] deriv f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>L : Filter 𝕜<GOAL>HasDerivAtFilter id 1 x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>HasDerivWithinAt id 1 s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>HasDerivAt id 1 x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>HasDerivAt (fun x => x) 1 x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>HasStrictDerivAt id 1 x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>deriv id x = 1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<GOAL>deriv id = fun x => 1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<GOAL>(deriv fun x => x) = fun x => 1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin id s x = 1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>c : F<GOAL>HasDerivAtFilter (fun x => c) 0 x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>c : F<GOAL>HasStrictDerivAt (fun x => c) 0 x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>c : F<GOAL>HasDerivWithinAt (fun x => c) 0 s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>c : F<GOAL>HasDerivAt (fun x => c) 0 x