const_smul — Mathlib

English

A scalar multiple of a function that is harmonic on a neighborhood of s is harmonic on that neighborhood.

Русский

Умножение на скаляр гармоничной функции в окрестности s сохраняет гармоничность в этой окрестности.

LaTeX

$$$\operatorname{HarmonicOnNhd}(f,s) \Rightarrow \operatorname{HarmonicOnNhd}(c\cdot f,s)$$$

Lean4

/-- Scalar multiples of harmonic functions are harmonic.
-/
theorem const_smul (h : HarmonicOnNhd f s) : HarmonicOnNhd (c • f) s := fun x hx ↦ (h x hx).const_smul

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