tendsto_inv_nhdsGT — Mathlib

English

In an ordered topological group with continuous inversion, the map inv is one-sided continuous from above: Tendsto inv from nhdsWithin a from the upper side Ioi a to nhdsWithin a⁻¹ from the lower side Iio a⁻¹.

Русский

В упорядоченной топологической группе с непрерывной инверсией отображение инверсии имеет одностороннюю непрерывность: Tendsto inv с nhdsWithin a сверху к nhdsWithin a⁻¹ снизу.

LaTeX

$$$\text{Tendsto inv} (nhdsWithin\ a\ (Ioi\ a))\ (nhdsWithin\ a^{-1}\ (Iio\ a^{-1})).$$$

Lean4

@[to_additive]
theorem tendsto_inv_nhdsGT {a : H} : Tendsto Inv.inv (𝓝[>] a) (𝓝[<] a⁻¹) :=
  (continuous_inv.tendsto a).inf <| by simp

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