div_const — Mathlib

English

If f is ContDiff 𝕜 n, then y ↦ f(y)/c is ContDiff 𝕜 n for any constant c.

Русский

Если f гладкая, то f/c гладкая для любой константы c.

LaTeX

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

Lean4

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

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