div — Mathlib

English

Inversion preserves ContMDiffWithinAt under left-invariant derivations context.

Русский

Обращение сохраняет ContMDiffWithinAt в контексте левых инвариантных выводов.

LaTeX

$$ContMDiffWithinAt I' I n f s x0 → ContMDiffWithinAt I' I n (inv f) s x0$$

Lean4

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

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