smul — Mathlib

English

If f is ContDiffWithinAt 𝕜 n f s x, then ∀ m ∈ ℕ, f^m is ContDiffWithinAt 𝕜 n at s, x.

Русский

Если f гладко внутри s в x, то f^m гладко внутри s в x для любого m.

LaTeX

$$$\\\\forall m \\\\in \\\\mathbb{N}, \\\\ ContDiffWithinAt 𝕜 n f s x \\\\Rightarrow \\\\ ContDiffWithinAt 𝕜 n (f^m) s x$$

Lean4

/-- The scalar multiplication of two `C^n` functions within a set at a point is `C^n` within this
set at this point. -/
@[fun_prop]
theorem smul {s : Set E} {f : E → 𝕜} {g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
    ContDiffWithinAt 𝕜 n (fun x => f x • g x) s x :=
  contDiff_smul.contDiffWithinAt.comp x (hf.prodMk hg) subset_preimage_univ

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