tendsto_inv_nhdsGE_inv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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