div₀ — Mathlib

English

If hf and hg are C^n on s and g is nowhere zero on s, then f/g is C^n on s.

Русский

Если hf и hg гладкие на 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 : ContMDiff I' I n f) (hg : ContMDiff I' I n g) (h₀ : ∀ x, g x ≠ 0) : ContMDiff I' I n (f / g) := by
  simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

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