contMDiff_congr — Mathlib

English

If f is ContMDiffAt and f1 =ᶠ[nhds x] f, then ContMDiffAt I I' n f1 x.

Русский

Если f гладкая в x, и f1 совпадает с f в окрестности x почти наверняка, то f1 гладкая в x.

LaTeX

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

Lean4

theorem contMDiff_congr (h₁ : ∀ y, f₁ y = f y) : ContMDiff I I' n f₁ ↔ ContMDiff I I' n f :=
  by
  simp_rw [← contMDiffOn_univ]
  exact contMDiffOn_congr fun y _ ↦ h₁ y

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