laplacianWithin_smul_nhds — Mathlib

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

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