tendsto_inv_nhdsLT — Mathlib

English

In the same setting, tendsto holds with the left-hand counterpart: Tendsto inv from nhdsWithin a from the lower side Iio a to nhdsWithin a⁻¹ from the upper side Ioi a⁻¹.

Русский

В той же конфигурации существует предел с левой стороны: Tendsto inv от nhdsWithin a по нижней границе к nhdsWithin a⁻¹ по верхней границе.

LaTeX

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

Lean4

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

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