laplacianWithin_congr_nhdsWithin — Mathlib

English

If two functions agree in a neighborhood, their Laplacians agree in a neighborhood.

Русский

Если две функции совпадают в окрестности точки, их лапласианы совпадают в окрестности этой точки.

LaTeX

$$nhds_nhdsWithin_eq (h) (hs) : Δ f1 = Δ f2 in nhds$$

Lean4

/-- If two functions agree in a neighborhood of a point, then so do their Laplacians.
-/
theorem laplacianWithin_congr_nhdsWithin (h : f₁ =ᶠ[𝓝[s] x] f₂) (hs : UniqueDiffOn ℝ s) : Δ[s]f₁ =ᶠ[𝓝[s] x] Δ[s]f₂ :=
  by
  filter_upwards [EventuallyEq.iteratedFDerivWithin (𝕜 := ℝ) h 2, eventually_mem_nhdsWithin] with x h₁x h₂x
  simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs h₂x, h₁x]

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