English
If f is continuous and never zero, then x ↦ f(x)⁻¹ is continuous everywhere.
Русский
Если f непрерывна и нигде не равна нулю, то обратная функция непрерывна на всем домене.
LaTeX
$$Continuous f → (∀ x, f x ≠ 0) → Continuous (\\lambda x, f(x)^{-1})$$
Lean4
/-- The function `f x / g x` is discontinuous when `g x = 0`. However, under appropriate
conditions, `h x (f x / g x)` is still continuous. The condition is that if `g a = 0` then `h x y`
must tend to `h a 0` when `x` tends to `a`, with no information about `y`. This is represented by
the `⊤` filter. Note: `tendsto_prod_top_iff` characterizes this convergence in uniform spaces. See
also `Filter.prod_top` and `Filter.mem_prod_top`. -/
theorem comp_div_cases {f g : α → G₀} (h : α → G₀ → β) (hf : ContinuousAt f a) (hg : ContinuousAt g a)
(hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)) (h2h : g a = 0 → Tendsto ↿h (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))) :
ContinuousAt (fun x => h x (f x / g x)) a :=
by
change ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
by_cases hga : g a = 0
· rw [ContinuousAt]
simp_rw [comp_apply, hga, div_zero]
exact (h2h hga).comp (continuousAt_id.tendsto.prodMk tendsto_top)
· fun_prop (disch := assumption)
