English
Let c, R, x be functions with ContDiff Real n on s; if x(a) ≠ c(a) for all a, then the function a ↦ inversion(c(a), R(a), x(a)) is ContDiff Real n on s.
Русский
Пусть c, R, x — функции с ContDiff Real n на s; если x(a) ≠ c(a) для всех a, тогда a ↦ inversion(c(a), R(a), x(a)) имеет ContDiff Real n на s.
LaTeX
$$$\text{ContDiff}(Real,n,c,s) \land \text{ContDiff}(Real,n,R,s) \land \text{ContDiff}(Real,n,x,s) \land \forall a, x(a)\neq c(a) \Rightarrow \text{ContDiff}(Real,n, a\mapsto inversion(c(a),R(a),x(a)), s)$$$
Lean4
protected theorem inversion (hc : ContDiffOn ℝ n c s) (hR : ContDiffOn ℝ n R s) (hx : ContDiffOn ℝ n x s)
(hne : ∀ a ∈ s, x a ≠ c a) : ContDiffOn ℝ n (fun a ↦ inversion (c a) (R a) (x a)) s := fun a ha ↦
(hc a ha).inversion (hR a ha) (hx a ha) (hne a ha)
