tendsto_inv_nhdsLE_inv — Mathlib

English

Let H be a linearly ordered topological group with continuous inversion. Then, Tendsto inv (𝓝[≤] a⁻¹) (𝓝[≥] a).

Русский

Пусть H — упорядоченная топологическая группа с непрерывной инверсией. Тогда Tendsto inv (nhds≤ a⁻¹) (nhds≥ a).

LaTeX

$$$\forall a\,\in H:\; \operatorname{Tendsto} \mathrm{inv} \, (\mathcal{N}_{\le} a^{-1}) \, (\mathcal{N}_{\ge} a)$$$

Lean4

@[to_additive]
theorem tendsto_inv_nhdsLE_inv {a : H} : Tendsto Inv.inv (𝓝[≤] a⁻¹) (𝓝[≥] a) := by
  simpa only [inv_inv] using tendsto_inv_nhdsLE (a := a⁻¹)

Похожие утверждения