English
For every unit x in R, the inversion map a ↦ a^{-1} is continuous at a = x.
Русский
Для каждого единичного элемента x в R отображение a ↦ a^{-1} непрерывно в точке a = x.
LaTeX
$$$\\forall x \\in R^{\\times}, \\ \\lim_{a \\to x} a^{-1} = x^{-1}$$$
Lean4
/-- The function `Ring.inverse` is continuous at each unit of `R`. -/
theorem inverse_continuousAt (x : Rˣ) : ContinuousAt inverse (x : R) :=
by
have h_is_o : (fun t : R => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] (fun _ => 1 : R → ℝ) :=
(inverse_add_norm_diff_first_order x).trans_isLittleO (isLittleO_id_const one_ne_zero).norm_left
have h_lim : Tendsto (fun y : R => y - x) (𝓝 x) (𝓝 0) :=
by
refine tendsto_zero_iff_norm_tendsto_zero.mpr ?_
exact tendsto_iff_norm_sub_tendsto_zero.mp tendsto_id
rw [ContinuousAt, tendsto_iff_norm_sub_tendsto_zero, inverse_unit]
simpa [Function.comp_def] using h_is_o.norm_left.tendsto_div_nhds_zero.comp h_lim
