inverse — Mathlib

English

If h is differentiable on S and hz x is a unit for all x ∈ S, then the inverse map is differentiable on S.

Русский

Если h дифференцируема на S и для всех x ∈ S h(x) - единица, то обратная операция дифференцируема на S.

LaTeX

$$$\text{DifferentiableOn } 𝕜 h S \rightarrow \text{IsUnit }(h x) \Rightarrow \text{DifferentiableOn } 𝕜 (h(x)^{-1}) S$$$

Lean4

@[fun_prop]
theorem inverse (hf : DifferentiableOn 𝕜 h S) (hz : ∀ x ∈ S, IsUnit (h x)) :
    DifferentiableOn 𝕜 (fun x => Ring.inverse (h x)) S := fun x h => (hf x h).inverse (hz x h)

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