div — Mathlib

English

If f,g ContDiffOn on s and g x ≠ 0 for all x in s, then x ↦ f(x)/g(x) is ContDiffOn 𝕜 n on s.

Русский

Если f,g ∈ ContDiffOn 𝕜 n на s и g(x) ≠ 0 для всех x∈s, то x↦f(x)/g(x) — ContDiffOn 𝕜 n на s.

LaTeX

$$$\\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n\\ f\\ s \\to \\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n\\ g\\ s \\to (\\forall x\\in s, g(x)\\neq 0) \\Rightarrow \\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n\\ (x\\mapsto f(x)/g(x))\\ s$$$

Lean4

@[fun_prop]
nonrec theorem div {f g : E → 𝕜} {n} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) (hx : g x ≠ 0) :
    ContDiffAt 𝕜 n (fun x => f x / g x) x :=
  hf.div hg hx

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