isOpen_setOf_harmonicAt — Mathlib

English

If f is harmonic at x, then f is harmonic at all points in some neighborhood of x.

Русский

Если f гармонична в точке x, то она гармонична во всех точках некоторой окрестности x.

LaTeX

$$$\operatorname{HarmonicAt}(f,x) \Rightarrow \forall y\text{ near }x,\ \operatorname{HarmonicAt}(f,y)$$$

Lean4

/-- Harmonicity is an open property.
-/
theorem isOpen_setOf_harmonicAt : IsOpen {x : E | HarmonicAt f x} :=
  isOpen_iff_mem_nhds.2 (fun _ hx ↦ hx.eventually)

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