harmonicOnNhd_comp_CLE_iff — Mathlib

English

On applying a continuous linear equivalence, harmonicity on a neighborhood is preserved and vice versa.

Русский

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

LaTeX

$$$\operatorname{HarmonicOnNhd}(f,s) \iff \operatorname{HarmonicOnNhd}(l\circ f,s)$ for a continuous linear equivalence l.$$

Lean4

/-- Functions are harmonic iff their compositions with continuous linear equivalences are harmonic.
-/
theorem harmonicOnNhd_comp_CLE_iff (l : F ≃L[ℝ] G) : HarmonicOnNhd (l ∘ f) s ↔ HarmonicOnNhd f s :=
  forall₂_congr fun _ _ ↦ harmonicAt_comp_CLE_iff l

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