mono — Mathlib

English

If f is harmonic on a neighborhood of s and t ⊆ s, then f is harmonic on a neighborhood of t.

Русский

Если функция гармонична в окрестности множества s и t ⊆ s, то она гармонична в окрестности t.

LaTeX

$$$hf: \operatorname{HarmonicOnNhd}(f,s) \land t \subseteq s \Rightarrow \operatorname{HarmonicOnNhd}(f,t)$$$

Lean4

/-- If `f` is harmonic in a neighborhood of `s`, it is harmonic in a neighborhood of every subset.
-/
theorem mono (h : HarmonicOnNhd f s) (hst : t ⊆ s) : HarmonicOnNhd f t := fun x hx ↦ h x (hst hx)

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