neg — Mathlib

English

If f is C^n at a point x, then -f is C^n at that point.

Русский

Если функция f обладает C^n гладкостью в точке x, то −f тоже обладает C^n гладкостью в этой точке.

LaTeX

$$$ ContDiffAt 𝕜 n f x \Rightarrow ContDiffAt 𝕜 n (-f) x $$$

Lean4

/-- The negative of a `C^n` function at a point is `C^n` at this point. -/
@[fun_prop]
theorem neg {f : E → F} (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (fun x => -f x) x := by
  rw [← contDiffWithinAt_univ] at *; exact hf.neg

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