tendsto_inv_atBot_atTop — Mathlib

English

The inversion map sends Tendsto from atBot to atTop: Tendsto inv l atBot → Tendsto inv l atTop.

Русский

Инверсия переводит предел с atBot к atTop: Tendsto inv l atBot → Tendsto inv l atTop.

LaTeX

$$$\\mathrm{Tendsto}(\\mathrm{Inv.inv})\\ l\\ atBot\\rightarrow \\mathrm{Tendsto}(\\mathrm{Inv.inv})\\ l\\ atTop$$$

Lean4

@[to_additive]
theorem tendsto_inv_atBot_atTop : Tendsto (Inv.inv : G → G) atBot atTop :=
  tendsto_inv_atTop_atBot (G := Gᵒᵈ)

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