inv — Mathlib

English

If u is a Cauchy sequence in a group, then its inverse sequence u^{-1} is also Cauchy.

Русский

Если u — последовательность Коши в группе, то последовательность обратных элементов u^{-1} тоже является последовательностью Коши.

LaTeX

$$$CauchySeq\\,u \\Rightarrow CauchySeq\\,u^{-1}$$$

Lean4

@[to_additive]
theorem inv {ι : Type*} [Preorder ι] {u : ι → α} (h : CauchySeq u) : CauchySeq u⁻¹ :=
  uniformContinuous_inv.comp_cauchySeq h

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