English
Construct a unit from limits of units and their inverses: given a net f: ι → Units N with f converging to r1 and f⁻¹ converging to r2, one obtains a unit with value r1 and inverse value r2.
Русский
Построение единицы из пределов единиц и их обратных: если сеть f: ι → Units N сходится к r1, а сеть обратных значений сходится к r2, то существует элемент-единица с значением r1 и обратной величиной r2.
LaTeX
$$$\text{units} : (f: ι \to \mathrm{Units}(N))\to (r_1,r_2) \,\text{сводится к} \, N^×$$$
Lean4
/-- Construct a unit from limits of units and their inverses. -/
@[to_additive (attr := simps) /-- Construct an additive unit from limits of additive units and their negatives. -/
]
def units [TopologicalSpace N] [Monoid N] [ContinuousMul N] [T2Space N] {f : ι → Nˣ} {r₁ r₂ : N} {l : Filter ι}
[l.NeBot] (h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁)) (h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)) : Nˣ
where
val := r₁
inv := r₂
val_inv := by
symm
simpa using h₁.mul h₂
inv_val := by
symm
simpa using h₂.mul h₁
