tendsto_inv_cobounded — Mathlib

English

The inv operation preserves cobounded: (cobounded E)⁻¹ = cobounded E.

Русский

Операция взятия обратной сохраняет cobounded: (cobounded E)⁻¹ = cobounded E.

LaTeX

$$(cobounded E)^{-1} = cobounded E$$

Lean4

/-- In a (semi)normed group, inversion `x ↦ x⁻¹` tends to infinity at infinity. -/
@[to_additive /-- In a (semi)normed group, negation `x ↦ -x` tends to infinity at infinity. -/
    ]
theorem tendsto_inv_cobounded : Tendsto Inv.inv (cobounded E) (cobounded E) :=
  inv_cobounded.le

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