The Fréchet derivative: congruence properties #
Lemmas about congruence properties of the Fréchet derivative under change of function, set, etc.
Tags #
derivative, differentiable, Fréchet, calculus
congr properties of the derivative #
theorem
hasFDerivWithinAt_congr_set_nhdsNE
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s t : Set E}
(h : s =ᶠ[nhdsWithin x {x}ᶜ] t)
:
theorem
hasFDerivWithinAt_congr_set
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s t : Set E}
(h : s =ᶠ[nhds x] t)
:
theorem
hasFDerivWithinAt_congr_set'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s t : Set E}
[T1Space E]
(y : E)
(h : s =ᶠ[nhdsWithin x {y}ᶜ] t)
:
In the case y = x, see also hasFDerivWithinAt_congr_set_nhdsNE,
which does not require the domain to be a T₁ space.
theorem
differentiableWithinAt_congr_set_nhdsNE
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{x : E}
{s t : Set E}
(h : s =ᶠ[nhdsWithin x {x}ᶜ] t)
:
theorem
differentiableWithinAt_congr_set'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{x : E}
{s t : Set E}
[T1Space E]
(y : E)
(h : s =ᶠ[nhdsWithin x {y}ᶜ] t)
:
In the case y = x, see also differentiableWithinAt_congr_set_nhdsNE,
which does not require the domain to be a T₁ space.
theorem
differentiableWithinAt_congr_set
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{x : E}
{s t : Set E}
(h : s =ᶠ[nhds x] t)
:
theorem
fderivWithin_congr_set_nhdsNE
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{x : E}
{s t : Set E}
(h : s =ᶠ[nhdsWithin x {x}ᶜ] t)
:
theorem
fderivWithin_congr_set'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{x : E}
{s t : Set E}
[T1Space E]
(y : E)
(h : s =ᶠ[nhdsWithin x {y}ᶜ] t)
:
In the case y = x, see also fderivWithin_congr_set_nhdsNE,
which does not require the domain to be a T₁ space.
theorem
fderivWithin_congr_set
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{x : E}
{s t : Set E}
(h : s =ᶠ[nhds x] t)
:
theorem
fderivWithin_eventually_congr_set'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{x : E}
{s t : Set E}
[T1Space E]
(y : E)
(h : s =ᶠ[nhdsWithin x {y}ᶜ] t)
:
theorem
fderivWithin_eventually_congr_set
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{x : E}
{s t : Set E}
(h : s =ᶠ[nhds x] t)
:
theorem
Filter.EventuallyEq.hasFDerivAtFilter_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f₀ f₁ : E → F}
{f₀' f₁' : E →L[𝕜] F}
{L : Filter (E × E)}
(h₀ : Prod.map f₀ f₀ =ᶠ[L] Prod.map f₁ f₁)
(h₁ : ∀ (x : E), f₀' x = f₁' x)
:
theorem
Filter.EventuallyEq.hasStrictFDerivAt_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f₀ f₁ : E → F}
{f₀' f₁' : E →L[𝕜] F}
{x : E}
(h : f₀ =ᶠ[nhds x] f₁)
(h' : ∀ (y : E), f₀' y = f₁' y)
:
theorem
HasStrictFDerivAt.congr_fderiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{f' g' : E →L[𝕜] F}
{x : E}
(h : HasStrictFDerivAt f f' x)
(h' : f' = g')
:
HasStrictFDerivAt f g' x
theorem
HasFDerivAt.congr_fderiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{f' g' : E →L[𝕜] F}
{x : E}
(h : HasFDerivAt f f' x)
(h' : f' = g')
:
HasFDerivAt f g' x
theorem
HasFDerivWithinAt.congr_fderiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f : E → F}
{f' g' : E →L[𝕜] F}
{x : E}
{s : Set E}
(h : HasFDerivWithinAt f f' s x)
(h' : f' = g')
:
HasFDerivWithinAt f g' s x
theorem
HasStrictFDerivAt.congr_of_eventuallyEq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{f' : E →L[𝕜] F}
{x : E}
(h : HasStrictFDerivAt f f' x)
(h₁ : f =ᶠ[nhds x] f₁)
:
HasStrictFDerivAt f₁ f' x
theorem
HasFDerivAtFilter.congr_of_eventuallyEq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{f' : E →L[𝕜] F}
{L : Filter (E × E)}
(h : HasFDerivAtFilter f f' L)
(hL : Prod.map f₁ f₁ =ᶠ[L] Prod.map f f)
:
HasFDerivAtFilter f₁ f' L
theorem
Filter.EventuallyEq.hasFDerivAt_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f₀ f₁ : E → F}
{f' : E →L[𝕜] F}
{x : E}
(h : f₀ =ᶠ[nhds x] f₁)
:
theorem
Filter.EventuallyEq.differentiableAt_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f₀ f₁ : E → F}
{x : E}
(h : f₀ =ᶠ[nhds x] f₁)
:
theorem
Filter.EventuallyEq.hasFDerivWithinAt_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f₀ f₁ : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s : Set E}
(h : f₀ =ᶠ[nhdsWithin x s] f₁)
(hx : f₀ x = f₁ x)
:
theorem
Filter.EventuallyEq.hasFDerivWithinAt_iff_of_mem
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f₀ f₁ : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s : Set E}
(h : f₀ =ᶠ[nhdsWithin x s] f₁)
(hx : x ∈ s)
:
theorem
Filter.EventuallyEq.differentiableWithinAt_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f₀ f₁ : E → F}
{x : E}
{s : Set E}
(h : f₀ =ᶠ[nhdsWithin x s] f₁)
(hx : f₀ x = f₁ x)
:
theorem
Filter.EventuallyEq.differentiableWithinAt_iff_of_mem
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f₀ f₁ : E → F}
{x : E}
{s : Set E}
(h : f₀ =ᶠ[nhdsWithin x s] f₁)
(hx : x ∈ s)
:
theorem
HasFDerivWithinAt.congr_of_eventuallyEq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s : Set E}
(h : HasFDerivWithinAt f f' s x)
(h₁ : f₁ =ᶠ[nhdsWithin x s] f)
(hx : f₁ x = f x)
:
HasFDerivWithinAt f₁ f' s x
theorem
HasFDerivWithinAt.congr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s : Set E}
(h : HasFDerivWithinAt f f' s x)
(hs : Set.EqOn f₁ f s)
(hx : f₁ x = f x)
:
HasFDerivWithinAt f₁ f' s x
theorem
HasFDerivWithinAt.congr'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s : Set E}
(h : HasFDerivWithinAt f f' s x)
(hs : Set.EqOn f₁ f s)
(hx : x ∈ s)
:
HasFDerivWithinAt f₁ f' s x
theorem
HasFDerivWithinAt.congr_mono
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s t : Set E}
(h : HasFDerivWithinAt f f' s x)
(ht : Set.EqOn f₁ f t)
(hx : f₁ x = f x)
(h₁ : t ⊆ s)
:
HasFDerivWithinAt f₁ f' t x
theorem
HasFDerivAt.congr_of_eventuallyEq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{f' : E →L[𝕜] F}
{x : E}
(h : HasFDerivAt f f' x)
(h₁ : f₁ =ᶠ[nhds x] f)
:
HasFDerivAt f₁ f' x
theorem
DifferentiableWithinAt.congr_mono
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s t : Set E}
(h : DifferentiableWithinAt 𝕜 f s x)
(ht : Set.EqOn f₁ f t)
(hx : f₁ x = f x)
(h₁ : t ⊆ s)
:
DifferentiableWithinAt 𝕜 f₁ t x
theorem
DifferentiableWithinAt.congr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s : Set E}
(h : DifferentiableWithinAt 𝕜 f s x)
(ht : ∀ x ∈ s, f₁ x = f x)
(hx : f₁ x = f x)
:
DifferentiableWithinAt 𝕜 f₁ s x
theorem
DifferentiableWithinAt.congr_of_eventuallyEq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s : Set E}
(h : DifferentiableWithinAt 𝕜 f s x)
(h₁ : f₁ =ᶠ[nhdsWithin x s] f)
(hx : f₁ x = f x)
:
DifferentiableWithinAt 𝕜 f₁ s x
theorem
DifferentiableWithinAt.congr_of_eventuallyEq_of_mem
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s : Set E}
(h : DifferentiableWithinAt 𝕜 f s x)
(h₁ : f₁ =ᶠ[nhdsWithin x s] f)
(hx : x ∈ s)
:
DifferentiableWithinAt 𝕜 f₁ s x
theorem
DifferentiableWithinAt.congr_of_eventuallyEq_insert
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s : Set E}
(h : DifferentiableWithinAt 𝕜 f s x)
(h₁ : f₁ =ᶠ[nhdsWithin x (insert x s)] f)
:
DifferentiableWithinAt 𝕜 f₁ s x
theorem
DifferentiableOn.congr_mono
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{s t : Set E}
(h : DifferentiableOn 𝕜 f s)
(h' : ∀ x ∈ t, f₁ x = f x)
(h₁ : t ⊆ s)
:
DifferentiableOn 𝕜 f₁ t
theorem
DifferentiableOn.congr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{s : Set E}
(h : DifferentiableOn 𝕜 f s)
(h' : ∀ x ∈ s, f₁ x = f x)
:
DifferentiableOn 𝕜 f₁ s
theorem
differentiableOn_congr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{s : Set E}
(h' : ∀ x ∈ s, f₁ x = f x)
:
theorem
DifferentiableAt.congr_of_eventuallyEq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
(h : DifferentiableAt 𝕜 f x)
(hL : f₁ =ᶠ[nhds x] f)
:
DifferentiableAt 𝕜 f₁ x
theorem
DifferentiableWithinAt.fderivWithin_congr_mono
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s t : Set E}
[ContinuousAdd E]
[ContinuousSMul 𝕜 E]
[ContinuousAdd F]
[ContinuousSMul 𝕜 F]
[T2Space F]
(h : DifferentiableWithinAt 𝕜 f s x)
(hs : Set.EqOn f₁ f t)
(hx : f₁ x = f x)
(hxt : UniqueDiffWithinAt 𝕜 t x)
(h₁ : t ⊆ s)
:
theorem
Filter.EventuallyEq.fderivWithin_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s : Set E}
(hs : f₁ =ᶠ[nhdsWithin x s] f)
(hx : f₁ x = f x)
:
theorem
Filter.EventuallyEq.fderivWithin_eq_of_mem
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s : Set E}
(hs : f₁ =ᶠ[nhdsWithin x s] f)
(hx : x ∈ s)
:
theorem
Filter.EventuallyEq.fderivWithin_eq_of_insert
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s : Set E}
(hs : f₁ =ᶠ[nhdsWithin x (insert x s)] f)
:
theorem
Filter.EventuallyEq.fderivWithin'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s t : Set E}
(hs : f₁ =ᶠ[nhdsWithin x s] f)
(ht : t ⊆ s)
:
theorem
Filter.EventuallyEq.fderivWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s : Set E}
(hs : f₁ =ᶠ[nhdsWithin x s] f)
:
theorem
Filter.EventuallyEq.fderivWithin_eq_of_nhds
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s : Set E}
(h : f₁ =ᶠ[nhds x] f)
:
theorem
fderivWithin_congr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s : Set E}
(hs : Set.EqOn f₁ f s)
(hx : f₁ x = f x)
:
theorem
fderivWithin_congr'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
{s : Set E}
(hs : Set.EqOn f₁ f s)
(hx : x ∈ s)
:
theorem
Filter.EventuallyEq.fderiv_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
(h : f₁ =ᶠ[nhds x] f)
:
theorem
Filter.EventuallyEq.fderiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{x : E}
(h : f₁ =ᶠ[nhds x] f)
:
theorem
Filter.EventuallyEq.codiscreteWithin_fderivWithin'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{s t : Set E}
(h : f₁ =ᶠ[codiscreteWithin s] f)
(ht : t ⊆ s)
:
If two functions agree on a codiscrete subset of s, then so do their derivatives within
any subset t of s.
theorem
Filter.EventuallyEq.codiscreteWithin_fderivWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{s : Set E}
(h : f₁ =ᶠ[codiscreteWithin s] f)
:
If two functions agree on a codiscrete subset of s, then so do their derivatives
within s.
theorem
Filter.EventuallyEq.codiscreteWithin_fderiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{s : Set E}
(h : f₁ =ᶠ[codiscreteWithin s] f)
(hs : IsOpen s)
:
If two functions agree on a codiscrete subset of an open set s, then so do their
derivatives.
theorem
Filter.EventuallyEq.codiscrete_fderivWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
{s : Set E}
(h : f₁ =ᶠ[codiscrete E] f)
:
If two functions agree on a codiscrete subset of E, then so do their derivatives within
any subset s of E.
theorem
Filter.EventuallyEq.codiscrete_fderiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{F : Type u_3}
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
{f f₁ : E → F}
(h : f₁ =ᶠ[codiscrete E] f)
:
If two functions agree on a codiscrete subset of E, then so do their derivatives.