inversion — Mathlib

English

If c, R, x are differentiable on a set s and x(a) ≠ c(a) for all a ∈ s, then the composed inversion is differentiable on s.

Русский

Если c, R и x дифференцируемы на s и x(a) ≠ c(a) для всех a ∈ s, то композиция инверсии дифференцируема на s.

LaTeX

$$DifferentiableOn Real c s ∧ DifferentiableOn Real R s ∧ DifferentiableOn Real x s ∧ ∀ a ∈ s, x a ≠ c a ⇒ DifferentiableOn Real (a ↦ inversion (c a) (R a) (x a)) s$$

Lean4

protected theorem inversion (hc : DifferentiableOn ℝ c s) (hR : DifferentiableOn ℝ R s) (hx : DifferentiableOn ℝ x s)
    (hne : ∀ a ∈ s, x a ≠ c a) : DifferentiableOn ℝ (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)

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