English
Let H be a linearly ordered topological group with continuous inversion. Then, for every a ∈ H, the inversion map sends the nonnegative neighborhood of a to the nonpositive neighborhood of a⁻¹ from the other side; i.e., Tendsto inv (𝓝[≥] a) (𝓝[≤] a⁻¹).
Русский
Пусть H — упорядоченная топологическая группа с непрерывной инверсией. Тогда для любого a ∈ H отображение x ↦ x⁻¹ переводит окрестности слева от a в окрестности справа от a⁻¹ и наоборот, формулировка: Tendsto inv (𝓝[≥] a) (𝓝[≤] a⁻¹).
LaTeX
$$$\forall a\,\in H:\; \operatorname{Tendsto} \mathrm{inv} \ (\mathcal{N}_{\ge} a)\ (\mathcal{N}_{\le} a^{-1})$$$
Lean4
@[to_additive]
theorem tendsto_inv_nhdsGE {a : H} : Tendsto Inv.inv (𝓝[≥] a) (𝓝[≤] a⁻¹) :=
(continuous_inv.tendsto a).inf <| by simp
