div_const — Mathlib

English

If f is ContDiffAt 𝕜 n f x, then y ↦ f(y)/c is ContDiffAt 𝕜 n at x for any nonzero c.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
nonrec theorem div_const {f : E → 𝕜'} {n} (hf : ContDiffAt 𝕜 n f x) (c : 𝕜') : ContDiffAt 𝕜 n (fun x => f x / c) x :=
  hf.div_const c

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