div₀ — Mathlib

English

If f and g are C^n on s and g is nowhere zero on 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\in s, g(x) \neq 0) \Rightarrow \ContMDiffOn I' I n (\lambda x \mapsto \tfrac{f(x)}{g(x)}) s $$$$

Lean4

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

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