add — Mathlib

English

If f1 and f2 are harmonic on a neighborhood of s, then f1+f2 is harmonic on a neighborhood of s.

Русский

Если f1 и f2 гармоничны в окрестности s, то их сумма гармонична в окрестности s.

LaTeX

$$$\operatorname{HarmonicOnNhd}(f_1,s) \land \operatorname{HarmonicOnNhd}(f_2,s) \Rightarrow \operatorname{HarmonicOnNhd}(f_1+f_2,s)$$$

Lean4

/-- Sums of harmonic functions are harmonic.
-/
theorem add (h₁ : HarmonicOnNhd f₁ s) (h₂ : HarmonicOnNhd f₂ s) : HarmonicOnNhd (f₁ + f₂) s := fun x hx ↦
  (h₁ x hx).add (h₂ x hx)

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