English
Let v ∈ ℝ and f be ContDiffWithinAt Real 2 on s at x. Then Δ[s](v · f) =ᶠ[𝓝[s] x] v · Δ[s]f, i.e., the equality holds eventually in the nhdsWithin neighborhood of x within s.
Русский
Пусть v ∈ ℝ и f удовлетворяет ContDiffWithinAt Real 2 на s в точке x. Тогда Δ[s](v f) равно v·Δ[s]f не мгновенно, а в окрестности x внутри s.
LaTeX
$$$ Δ[s](v \cdot f) =^{}_{𝓝[s]x} v \cdot (Δ[s]f). $$$
Lean4
/-- The Laplacian commutes with scalar multiplication. -/
theorem laplacianWithin_smul_nhds (v : ℝ) (hf : ContDiffWithinAt ℝ 2 f s x) (hs : UniqueDiffOn ℝ s) :
Δ[s](v • f) =ᶠ[𝓝[s] x] v • (Δ[s]f) := by
filter_upwards [(hf.eventually (by simp)).filter_mono (nhdsWithin_mono _ (Set.subset_insert ..)),
eventually_mem_nhdsWithin] with a h₁a using laplacianWithin_smul v h₁a hs