laplacian_CLM_comp_left_nhds — Mathlib

English

Let l be a continuous linear map; then Δ(l ∘ f) =ᶠ[𝓝 x] l ∘ Δ f at x.

Русский

Пусть l — непрерывное линейное отображение; тогда Δ(l ∘ f) =ᶠ[𝓝 x] l ∘ Δ f в окрестности x.

LaTeX

$$$ Δ(l \circ f) =^{}_{\nhds x} l \circ (Δ f). $$$

Lean4

/-- The Laplacian commutes with left composition by continuous linear maps. -/
theorem _root_.ContDiffAt.laplacian_CLM_comp_left_nhds {l : F →L[ℝ] G} (h : ContDiffAt ℝ 2 f x) :
    Δ (l ∘ f) =ᶠ[𝓝 x] l ∘ (Δ f) := by
  filter_upwards [h.eventually (by simp)] with a ha
  rw [ha.laplacian_CLM_comp_left]

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