inv — Mathlib

English

If f and g are ContMDiffWithinAt on s near x0, then x ↦ f(x)/g(x) is ContMDiffWithinAt on s near x0.

Русский

Если f и g гладко дифференцируемы в пределах s около x0, то x ↦ f(x)/g(x) гладко дифференцируемо около x0.

LaTeX

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

Lean4

@[to_additive]
theorem inv {f : M → G} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) :
    ContMDiffWithinAt I' I n (fun x => (f x)⁻¹) s x₀ :=
  (contMDiff_inv I n).contMDiffAt.contMDiffWithinAt.comp x₀ hf <| Set.mapsTo_univ _ _

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