English
Let H be a linearly ordered topological group with continuous inversion. Then, for any a ∈ H, the inversion map sends the ≤-neighborhood of a to the ≥-neighborhood of a⁻¹; 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}_{\le} a) \, (\mathcal{N}_{\ge} a^{-1})$$$
Lean4
@[to_additive]
theorem tendsto_inv_nhdsLE {a : H} : Tendsto Inv.inv (𝓝[≤] a) (𝓝[≥] a⁻¹) :=
(continuous_inv.tendsto a).inf <| by simp
