tendsto_inv_nhdsGT_inv — Mathlib

English

For any a ∈ H with continuous inversion, Tendsto inv from nhdsWithin (inv a) (Ioi inv a) to nhdsWithin a (Iio a) holds; equivalently, the same with a replaced by a⁻¹.

Русский

Для любого a с непрерывной инверсией существует Tendsto inv от nhdsWithin (inv a) к Ioi inv a в nhdsWithin a к Iio a; эквивалентно аналогично после замены a на a⁻¹.

LaTeX

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

Lean4

@[to_additive]
theorem tendsto_inv_nhdsGT_inv {a : H} : Tendsto Inv.inv (𝓝[>] a⁻¹) (𝓝[<] a) := by
  simpa only [inv_inv] using tendsto_inv_nhdsGT (a := a⁻¹)

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