div — Mathlib

English

If f and g are ContMDiffAt at a point, then f/g is ContMDiffAt there as well.

Русский

Если f и g гладкие в точке, то и f/g гладко в этой точке.

LaTeX

$$ContMDiffAt I' I n f x0 → ContMDiffAt I' I n g x0 → ContMDiffAt I' I n (f/g) x0$$

Lean4

@[to_additive]
theorem div {f g : M → G} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) (hg : ContMDiffAt I' I n g x₀) :
    ContMDiffAt I' I n (fun x => f x / g x) x₀ := by simp_rw [div_eq_mul_inv]; exact hf.mul hg.inv

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