English
Let c and d be differentiable on a set s, and assume that d never vanishes on s. Then the quotient c/d is differentiable on s.
Русский
Пусть c и d дифференцируемы на множестве s, и предположим, что на s d(x) ≠ 0 для всех x. Тогда дробь c/d дифференцируема на s.
LaTeX
$$$ (\\mathrm{DifferentiableOn}_{\\mathbb{K}}\\; c\\; s) \\land (\\mathrm{DifferentiableOn}_{\\mathbb{K}}\\; d\\; s) \\land (\\forall x \\in s,\\; d(x) \\neq 0) \\Rightarrow \\mathrm{DifferentiableOn}_{\\mathbb{K}}(c/d)\\; s $$$
Lean4
@[fun_prop]
theorem div (hc : DifferentiableOn 𝕜 c s) (hd : DifferentiableOn 𝕜 d s) (hx : ∀ x ∈ s, d x ≠ 0) :
DifferentiableOn 𝕜 (c / d) s := fun x h => (hc x h).div (hd x h) (hx x h)
