div₀ — Mathlib

English

If f and g are C^n within at a on s and g(a) ≠ 0, then the quotient f/g is C^n within at a on s.

Русский

Если функции f и g имеют гладкость класса C^n в окрестности точки a на множестве s и g(a) ≠ 0, то частное f/g также гладко в окрестности a на s.

LaTeX

$$$$ \ContMDiffWithinAt I' I n f s a \land \ContMDiffWithinAt I' I n g s a \land g(a) \neq 0 \Rightarrow \ContMDiffWithinAt I' I n \bigl(\lambda x \mapsto \tfrac{f(x)}{g(x)}\bigr) s a $$$$

Lean4

theorem div₀ (hf : ContMDiffWithinAt I' I n f s a) (hg : ContMDiffWithinAt I' I n g s a) (h₀ : g a ≠ 0) :
    ContMDiffWithinAt I' I n (f / g) s a := by simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

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