congr_of_eventuallyEq — Mathlib

English

ContMDiffAt is invariant under almost everywhere equality: if f1 =ᶠ at x with f, then ContMDiffAt I I' n f1 x ↔ ContMDiffAt I I' n f x.

Русский

ContMDiffAt не зависит от значения функции на множества, равного почти наверняка в окрестности x.

LaTeX

$$$ (nhds x).EventuallyEq f1 f \Rightarrow ContMDiffAt I I' n f1 x \Leftrightarrow ContMDiffAt I I' n f x$$

Lean4

theorem congr_of_eventuallyEq (h : ContMDiffAt I I' n f x) (h₁ : f₁ =ᶠ[𝓝 x] f) : ContMDiffAt I I' n f₁ x :=
  (contDiffWithinAt_localInvariantProp n).liftPropAt_congr_of_eventuallyEq h h₁

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