comp_CLM — Mathlib

English

Composing with a continuous linear map preserves harmonicity on a neighborhood.

Русский

Сочетание с непрерывно линейным отображением сохраняет гармоничность на окрестности.

LaTeX

$$$\operatorname{HarmonicOnNhd}(f,s) \Rightarrow \operatorname{HarmonicOnNhd}(l\circ f,s)$$$

Lean4

/-- Compositions of continuous linear maps with harmonic functions are harmonic.
-/
theorem comp_CLM (h : HarmonicOnNhd f s) (l : F →L[ℝ] G) : HarmonicOnNhd (l ∘ f) s := fun x hx ↦ (h x hx).comp_CLM l

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