div₀ — Mathlib

English

If f and g are C^n on s and g is nonzero at every point of s, then f/g is C^n on s.

Русский

Если f и g гладкие на s класса C^n и g не обращается в нуль на всей области s, то f/g гладко на s.

LaTeX

$$$$ \ContMDiffOn I' I n f s \land \ContMDiffOn I' I n g s \land (\forall x, g(x) \neq 0) \Rightarrow \ContMDiffOn I' I n (\lambda x \mapsto \tfrac{f(x)}{g(x)}) s $$$$

Lean4

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

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