harmonicAt_congr_nhds — Mathlib

English

If two functions agree in a neighborhood of x, then harmonicity at x is equivalent for the two functions.

Русский

Если две функции совпадают в окрестности точки x, то в точке x гармоничность сохраняется и эквивалентна между ними.

LaTeX

$$$f_1=f_2\text{ in }\mathcal{N}(x) \Rightarrow \operatorname{HarmonicAt}(f_1,x) \iff \operatorname{HarmonicAt}(f_2,x)$$$

Lean4

/-- If two functions agree in a neighborhood of `x`, then one is harmonic at `x` iff so is the other.
-/
theorem harmonicAt_congr_nhds {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[𝓝 x] f₂) : HarmonicAt f₁ x ↔ HarmonicAt f₂ x :=
  by
  constructor <;> intro hf
  · exact ⟨hf.1.congr_of_eventuallyEq h.symm, (laplacian_congr_nhds h.symm).trans hf.2⟩
  · exact ⟨hf.1.congr_of_eventuallyEq h, (laplacian_congr_nhds h).trans hf.2⟩

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