inv₀ — Mathlib

English

If f is continuous on a set s and f(x) ≠ 0 for every x ∈ s, then x ↦ f(x)⁻¹ is continuous on s.

Русский

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

LaTeX

$$ContinuousOn f s → (∀ x ∈ s, f x ≠ 0) → ContinuousOn (\\λ x, f(x)^{-1}) s$$

Lean4

@[fun_prop]
theorem inv₀ (hf : ContinuousOn f s) (h0 : ∀ x ∈ s, f x ≠ 0) : ContinuousOn (fun x => (f x)⁻¹) s := fun x hx =>
  (hf x hx).inv₀ (h0 x hx)

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