inv — Mathlib

English

If f is differentiable on s and f(x) ≠ 0 for all x in closure s, then f⁻¹ is differentiable on s.

Русский

Если f дифференцируема на s и f(x) ≠ 0 для всех x в замыкании s, то f⁻¹ дифференцируема на s.

LaTeX

$$$\forall f:\, \text{DiffContOnCl}(𝕜, f, s) \land \forall x ∈ \overline{s}, f(x) \neq 0 \Rightarrow \text{DiffContOnCl}(𝕜, f^{-1}, s).$$$

Lean4

theorem inv {f : E → 𝕜} (hf : DiffContOnCl 𝕜 f s) (h₀ : ∀ x ∈ closure s, f x ≠ 0) : DiffContOnCl 𝕜 f⁻¹ s :=
  ⟨differentiableOn_inv.comp hf.1 fun _ hx => h₀ _ (subset_closure hx), hf.2.inv₀ h₀⟩

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