harmonicAt_comp_CLE_iff — Mathlib

English

A function is harmonic at x iff its composition with a continuous linear equivalence is harmonic at x.

Русский

Функция гармонична в точке x тогда и только тогда, когда композиция с непрерывно-обратимым линейным отображением гармонична в x.

LaTeX

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

Lean4

/-- Functions are harmonic iff their compositions with continuous linear equivalences are harmonic.
-/
theorem harmonicAt_comp_CLE_iff (l : F ≃L[ℝ] G) : HarmonicAt (l ∘ f) x ↔ HarmonicAt f x :=
  by
  constructor <;> intro h
  · simpa [Function.comp_def] using h.comp_CLM l.symm.toContinuousLinearMap
  · exact h.comp_CLM l.toContinuousLinearMap

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