laplacianWithin_CLE_comp_left — Mathlib

English

Let l be a continuous linear equivalence F ≃L G. Then Δ[s](l ∘ f) equals l ∘ Δ[s]f at x, i.e., Laplacian commutes with left composition by a linear equivalence.

Русский

Пусть l — непрерывное линейное эквивалентность F ≃L G. Тогда Δ[s](l ∘ f) = l ∘ Δ[s]f в x.

LaTeX

$$$ Δ[s](l \circ f)(x) = (l \circ (Δ[s]f))(x). $$$

Lean4

/-- The Laplacian commutes with left composition by continuous linear equivalences. -/
theorem laplacianWithin_CLE_comp_left {l : F ≃L[ℝ] G} (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) :
    (Δ[s](l ∘ f)) x = (l ∘ (Δ[s]f)) x := by
  simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx, l.iteratedFDerivWithin_comp_left _ hs hx]

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