fun_inv — Mathlib

English

If h is differentiableOn S and h(x) ≠ 0 for all x ∈ S, then the pointwise inverse x ↦ (h(x))^{-1} is differentiableOn S.

Русский

Если h дифференцируема на S и для каждого x ∈ S выполняется h(x) ≠ 0, то x ↦ (h(x))^{-1} дифференцируема на S.

LaTeX

$$$\\text{DifferentiableOn}_{\\mathbb{K}}(h,S) \\;\\land\\; \\forall x\\in S,\\ h(x) \\neq 0 \\Rightarrow \\text{DifferentiableOn}_{\\mathbb{K}}(x \\mapsto (h(x))^{-1}, S)$$$

Lean4

@[fun_prop]
theorem fun_inv (hf : DifferentiableOn 𝕜 h S) (hz : ∀ x ∈ S, h x ≠ 0) : DifferentiableOn 𝕜 (fun x => (h x)⁻¹) S :=
  fun x h => (hf x h).inv (hz x h)

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