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