English
If a unit x is given and y is close to x (‖y−x‖ < ‖x⁻¹‖⁻¹), then y is itself a unit, and its Units structure is constructed from the nearby perturbation.
Русский
Если дана единица x и y близка к x (‖y−x‖ < ‖x⁻¹‖⁻¹), то y является единицей; конструируется единичная структура Units для y.
LaTeX
$$$\|y-x\| < \|x^{-1}\|^{-1} \Rightarrow y \in R^{\times}.$$$
Lean4
/-- In a normed ring with summable geometric series, an element `y` of distance less
than `‖x⁻¹‖⁻¹` from `x` is a unit. Here we construct its `Units` structure. -/
@[simps! val]
def ofNearby (x : Rˣ) (y : R) (h : ‖y - x‖ < ‖(↑x⁻¹ : R)‖⁻¹) : Rˣ :=
(x.add (y - x : R) h).copy y (by simp) _ rfl
