div — Mathlib

English

Division preserves ContMDiffOn: if f and g are ContMDiffOn on a set, so is f/g.

Русский

Деление сохраняет ContMDiffOn: если f и g гладкие на множестве, то и f/g гладко на этом множестве.

LaTeX

$$ContMDiffOn I' I n f s → ContMDiffOn I' I n g s → ContMDiffOn I' I n (fun x => f x / g x) s$$

Lean4

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

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