Documentation

Mathlib.Analysis.Calculus.FDeriv.Congr

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 #

source
theorem hasFDerivWithinAt_congr_set' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s t : Set E} (y : E) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) :
HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
source
theorem hasFDerivWithinAt_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s t : Set E} (h : s =ᶠ[nhds x] t) :
HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
source
theorem differentiableWithinAt_congr_set' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s t : Set E} (y : E) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) :
DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x
source
theorem differentiableWithinAt_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s t : Set E} (h : s =ᶠ[nhds x] t) :
DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x
source
theorem fderivWithin_congr_set' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s t : Set E} (y : E) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) :
fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
source
theorem fderivWithin_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s t : Set E} (h : s =ᶠ[nhds x] t) :
fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
source
theorem fderivWithin_eventually_congr_set' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s t : Set E} (y : E) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) :
fderivWithin 𝕜 f s =ᶠ[nhds x] fderivWithin 𝕜 f t
source
theorem fderivWithin_eventually_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s t : Set E} (h : s =ᶠ[nhds x] t) :
fderivWithin 𝕜 f s =ᶠ[nhds x] fderivWithin 𝕜 f t
source
theorem Filter.EventuallyEq.hasStrictFDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₀ f₁ : E → F} {f₀' f₁' : E →L[𝕜] F} {x : E} (h : f₀ =ᶠ[nhds x] f₁) (h' : ∀ (y : E), f₀' y = f₁' y) :
HasStrictFDerivAt f₀ f₀' x ↔ HasStrictFDerivAt f₁ f₁' x
source
theorem HasStrictFDerivAt.congr_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' g' : E →L[𝕜] F} {x : E} (h : HasStrictFDerivAt f f' x) (h' : f' = g') :
HasStrictFDerivAt f g' x
source
theorem HasFDerivAt.congr_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' g' : E →L[𝕜] F} {x : E} (h : HasFDerivAt f f' x) (h' : f' = g') :
HasFDerivAt f g' x
source
theorem HasFDerivWithinAt.congr_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem HasStrictFDerivAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem Filter.EventuallyEq.hasFDerivAtFilter_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₀ f₁ : E → F} {f₀' f₁' : E →L[𝕜] F} {x : E} {L : Filter E} (h₀ : f₀ =ᶠ[L] f₁) (hx : f₀ x = f₁ x) (h₁ : ∀ (x : E), f₀' x = f₁' x) :
HasFDerivAtFilter f₀ f₀' x L ↔ HasFDerivAtFilter f₁ f₁' x L
source
theorem HasFDerivAtFilter.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {f' : E →L[𝕜] F} {x : E} {L : Filter E} (h : HasFDerivAtFilter f f' x L) (hL : f₁ =ᶠ[L] f) (hx : f₁ x = f x) :
HasFDerivAtFilter f₁ f' x L
source
theorem Filter.EventuallyEq.hasFDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₀ f₁ : E → F} {f' : E →L[𝕜] F} {x : E} (h : f₀ =ᶠ[nhds x] f₁) :
HasFDerivAt f₀ f' x ↔ HasFDerivAt f₁ f' x
source
theorem Filter.EventuallyEq.differentiableAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₀ f₁ : E → F} {x : E} (h : f₀ =ᶠ[nhds x] f₁) :
DifferentiableAt 𝕜 f₀ x ↔ DifferentiableAt 𝕜 f₁ x
source
theorem Filter.EventuallyEq.hasFDerivWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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) :
HasFDerivWithinAt f₀ f' s x ↔ HasFDerivWithinAt f₁ f' s x
source
theorem Filter.EventuallyEq.hasFDerivWithinAt_iff_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₀ f₁ : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : f₀ =ᶠ[nhdsWithin x s] f₁) (hx : x ∈ s) :
HasFDerivWithinAt f₀ f' s x ↔ HasFDerivWithinAt f₁ f' s x
source
theorem Filter.EventuallyEq.differentiableWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₀ f₁ : E → F} {x : E} {s : Set E} (h : f₀ =ᶠ[nhdsWithin x s] f₁) (hx : f₀ x = f₁ x) :
DifferentiableWithinAt 𝕜 f₀ s x ↔ DifferentiableWithinAt 𝕜 f₁ s x
source
theorem Filter.EventuallyEq.differentiableWithinAt_iff_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₀ f₁ : E → F} {x : E} {s : Set E} (h : f₀ =ᶠ[nhdsWithin x s] f₁) (hx : x ∈ s) :
DifferentiableWithinAt 𝕜 f₀ s x ↔ DifferentiableWithinAt 𝕜 f₁ s x
source
theorem HasFDerivWithinAt.congr_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem HasFDerivWithinAt.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem HasFDerivWithinAt.congr' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem HasFDerivWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem HasFDerivAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem DifferentiableWithinAt.congr_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem DifferentiableWithinAt.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem DifferentiableWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem DifferentiableWithinAt.congr_of_eventuallyEq_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem DifferentiableWithinAt.congr_of_eventuallyEq_insert {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem DifferentiableOn.congr_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem DifferentiableOn.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {s : Set E} (h : DifferentiableOn 𝕜 f s) (h' : ∀ x ∈ s, f₁ x = f x) :
DifferentiableOn 𝕜 f₁ s
source
theorem differentiableOn_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {s : Set E} (h' : ∀ x ∈ s, f₁ x = f x) :
DifferentiableOn 𝕜 f₁ s ↔ DifferentiableOn 𝕜 f s
source
theorem DifferentiableAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} (h : DifferentiableAt 𝕜 f x) (hL : f₁ =ᶠ[nhds x] f) :
DifferentiableAt 𝕜 f₁ x
source
theorem DifferentiableWithinAt.fderivWithin_congr_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s t : Set E} (h : DifferentiableWithinAt 𝕜 f s x) (hs : Set.EqOn f₁ f t) (hx : f₁ x = f x) (hxt : UniqueDiffWithinAt 𝕜 t x) (h₁ : t ⊆ s) :
fderivWithin 𝕜 f₁ t x = fderivWithin 𝕜 f s x
source
theorem Filter.EventuallyEq.fderivWithin_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s : Set E} (hs : f₁ =ᶠ[nhdsWithin x s] f) (hx : f₁ x = f x) :
fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
source
theorem Filter.EventuallyEq.fderivWithin_eq_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s : Set E} (hs : f₁ =ᶠ[nhdsWithin x s] f) (hx : x ∈ s) :
fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
source
theorem Filter.EventuallyEq.fderivWithin_eq_of_insert {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s : Set E} (hs : f₁ =ᶠ[nhdsWithin x (insert x s)] f) :
fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
source
theorem Filter.EventuallyEq.fderivWithin' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s t : Set E} (hs : f₁ =ᶠ[nhdsWithin x s] f) (ht : t ⊆ s) :
fderivWithin 𝕜 f₁ t =ᶠ[nhdsWithin x s] fderivWithin 𝕜 f t
source
theorem Filter.EventuallyEq.fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s : Set E} (hs : f₁ =ᶠ[nhdsWithin x s] f) :
fderivWithin 𝕜 f₁ s =ᶠ[nhdsWithin x s] fderivWithin 𝕜 f s
source
theorem Filter.EventuallyEq.fderivWithin_eq_of_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s : Set E} (h : f₁ =ᶠ[nhds x] f) :
fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
source
@[deprecated Filter.EventuallyEq.fderivWithin_eq_of_nhds (since := "2025-05-20")]
theorem Filter.EventuallyEq.fderivWithin_eq_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s : Set E} (h : f₁ =ᶠ[nhds x] f) :
fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x

Alias of Filter.EventuallyEq.fderivWithin_eq_of_nhds.

source
theorem fderivWithin_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s : Set E} (hs : Set.EqOn f₁ f s) (hx : f₁ x = f x) :
fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
source
theorem fderivWithin_congr' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s : Set E} (hs : Set.EqOn f₁ f s) (hx : x ∈ s) :
fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
source
theorem Filter.EventuallyEq.fderiv_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} (h : f₁ =ᶠ[nhds x] f) :
fderiv 𝕜 f₁ x = fderiv 𝕜 f x
source
theorem Filter.EventuallyEq.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} (h : f₁ =ᶠ[nhds x] f) :
fderiv 𝕜 f₁ =ᶠ[nhds x] fderiv 𝕜 f