div_const — Mathlib

English

If f is ContDiffWithinAt 𝕜 n f s x and c ≠ 0, then y ↦ f(y)/c is ContDiffWithinAt 𝕜 n on s at x.

Русский

Если f гладко внутри s в x и константа c не равна нулю, то f/c гладко внутри s в x.

LaTeX

$$$\\\\forall c \\\\in \\\\mathbb{K}, \\\\ ContDiffWithinAt 𝕜 n f s x \\\\Rightarrow \\\\ ContDiffWithinAt 𝕜 n (\\\\lambda y. f(y)/c) s x$$

Lean4

@[fun_prop]
theorem div_const {f : E → 𝕜'} {n} (hf : ContDiffWithinAt 𝕜 n f s x) (c : 𝕜') :
    ContDiffWithinAt 𝕜 n (fun x => f x / c) s x := by simpa only [div_eq_mul_inv] using hf.mul contDiffWithinAt_const

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