HarmonicOnNhd — Mathlib

English

Let E be a real finite-dimensional inner product space and s a subset. A function is harmonic on a neighborhood of s if it is harmonic at every point of s.

Русский

Пусть E — вещественное конечномерное пространство с вложением и s — подмножество. Функция гармонична в окрестности s тогда, когда она гармонична в каждой точке s.

LaTeX

$$$\mathrm{HarmonicOnNhd}(f,s) \iff \forall x\in s, \operatorname{HarmonicAt}(f,x)$$$

Lean4

/-- Let `E` be a real, finite-dimensional, inner product space and `s` be a subset of `E`. A function
`f` on `E` is harmonic in a neighborhood of `s` if it is harmonic at every point of `s`.
-/
def HarmonicOnNhd :=
  ∀ x ∈ s, HarmonicAt f x

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