fun_div — Mathlib

English

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

Русский

Если f и g — ContDiffOn 𝕜 n на s и g(x) ≠ 0, то 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]
theorem fun_div {f g : E → 𝕜} {n} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) (h₀ : ∀ x ∈ s, g x ≠ 0) :
    ContDiffOn 𝕜 n (fun x => f x / g x) s :=
  ContDiffOn.div hf hg h₀

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