The Fréchet derivative: congruence properties #

Lemmas about congruence properties of the Frechet derivative under change of function, set, etc.

Tags #

derivative, differentiable, Fréchet, calculus

congr properties of the derivative #

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

Documentation

Mathlib.Analysis.Calculus.FDeriv.Congr

The Fréchet derivative: congruence properties #

Tags #

congr properties of the derivative #