congr_of_eventuallyEq — Mathlib

English

If f0 and f1 are eventually equal on nhdsWithin x s and x ∈ s, then LineDifferentiableWithinAt for f0 and f1 are equivalent on s at x in v.

Русский

Если f0 и f1 совпадают на nhdsWithin x s и x ∈ s, то линейная дифференцируемость внутри s эквивалентна между ними.

LaTeX

$$$(nhdsWithin x s).EventuallyEq f_{0} f_{1} \\land x \\in s \\Rightarrow \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f_{0},s;x,v) \\iff \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f_{1},s;x,v)$$$

Lean4

theorem congr_of_eventuallyEq (hf : HasLineDerivWithinAt 𝕜 f f' s x v) (h'f : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
    HasLineDerivWithinAt 𝕜 f₁ f' s x v :=
  h'f.symm.hasLineDerivWithinAt_iff hx.symm |>.mp hf

Похожие утверждения