English
Another formulation: if f and g are ContDiffOn 𝕜 n on s and g nonvanishing on s, then their quotient is ContDiffOn.
Русский
Еще одна формулировка: если f,g ∈ ContDiffOn 𝕜 n на s и g не обращается в ноль на s, то отношение f/g ∈ ContDiffOn 𝕜 n на s.
LaTeX
$$$\\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n\\ f\\ s \\to \\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n\\ g\\ s \\to (g\\text{ не обнуляется на } s) \\Rightarrow \\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n\\ (x\\mapsto f(x)/g(x))\\ s$$$
Lean4
@[fun_prop]
theorem div {f g : E → 𝕜} {n} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) (h0 : ∀ x, g x ≠ 0) :
ContDiff 𝕜 n fun x => f x / g x := by
simp only [contDiff_iff_contDiffAt] at *
exact fun x => (hf x).div (hg x) (h0 x)
