neg — Mathlib

English

If a function f is C^n within a domain s at x, then -f is also C^n within that domain at x.

Русский

Если функция f является C^n внутри области s в точке x, то -f тоже является C^n внутри этой области в точке x.

LaTeX

$$$ ContDiffWithinAt 𝕜 n f s x \Rightarrow ContDiffWithinAt 𝕜 n (-f) s x $$$

Lean4

/-- The negative of a `C^n` function within a domain at a point is `C^n` within this domain at
this point. -/
@[fun_prop]
theorem neg {s : Set E} {f : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (fun x => -f x) s x :=
  contDiff_neg.contDiffWithinAt.comp x hf subset_preimage_univ

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