eventually — Mathlib

English

The set of points where f is harmonic is open.

Русский

Множество точек, в которых функция гармонична, открыто.

LaTeX

$$$\{x:\,E\mid \operatorname{HarmonicAt}(f,x)\}$ is open.$$

Lean4

/-- If `f` is harmonic at `x`, then it is harmonic at all points in a neighborhood of `x`.
-/
theorem eventually {f : E → F} {x : E} (h : HarmonicAt f x) : ∀ᶠ y in 𝓝 x, HarmonicAt f y :=
  by
  filter_upwards [h.1.eventually (by simp), h.2.eventually_nhds] with a h₁a h₂a
  exact ⟨h₁a, h₂a⟩

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