English
Let H be a linearly ordered topological group with continuous inversion. Then, for every a in H, the inversion map x ↦ x⁻¹ sends left-neighborhoods of a⁻¹ into right-neighborhoods of a; equivalently, inv is continuous when approached from the left of a⁻¹ and observed from the right of a. In symbols: for all a, Tendsto inv (𝓝[<] a⁻¹) (𝓝[>] a).
Русский
Пусть H — упорядоченная топологическая группа с непрерывной инверсией. Тогда для каждого a ∈ H отображение x ↦ x⁻¹ переводит левую окрестность a⁻¹ в правую окрестность a; то есть предел inversion сохраняется слева. Формально: для всех a верно Tendsto inv (𝓝[<] a⁻¹) (𝓝[>] a).
LaTeX
Lean4
@[to_additive]
theorem tendsto_inv_nhdsLT_inv {a : H} : Tendsto Inv.inv (𝓝[<] a⁻¹) (𝓝[>] a) := by
simpa only [inv_inv] using tendsto_inv_nhdsLT (a := a⁻¹)
