Theorems · Theorem · real analysis

HasStrictDerivAt.congr_of_eventuallyEq

∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {x : 𝕜},
  HasStrictDerivAt f f' x → f =ᶠ[nhds x] f₁ → HasStrictDerivAt f₁ f' x

If f has derivative f' in the strict sense and f x' = f₁ x' near x, then f₁ has the same derivative in the strict sense. Note that this lemma assumes f =ᶠ[𝓝 x] f₁, while other lemmas in this file assume f₁ =ᶠ[𝓝 x] f. This is done for backward compatibility, and may change in the future. See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/MyProp.2Econgr_*.20lemmas.2C.20LHS.20vs.20RHS/with/572593573).

Defined in

Mathlib.Analysis.Calculus.Deriv.Basic

Cited by

7 results in Mathlib

Foundations

Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace