add — Mathlib

English

If f1 and f2 are harmonic at x, then their sum is harmonic at x.

Русский

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

LaTeX

$$$\operatorname{HarmonicAt}(f_1,x) \land \operatorname{HarmonicAt}(f_2,x) \Rightarrow \operatorname{HarmonicAt}(f_1+f_2,x)$$$

Lean4

/-- Sums of harmonic functions are harmonic.
-/
theorem add (h₁ : HarmonicAt f₁ x) (h₂ : HarmonicAt f₂ x) : HarmonicAt (f₁ + f₂) x :=
  by
  constructor
  · exact h₁.1.add h₂.1
  · filter_upwards [h₁.1.laplacian_add_nhds h₂.1, h₁.2, h₂.2]
    simp_all

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