totallyBounded_inv — Mathlib

English

If s is totally bounded in a uniform group, then its inverse set s^{-1} is totally bounded.

Русский

Если s полностью ограничено, то и множество обратных элементов s^{-1} полностью ограничено.

LaTeX

$$$TotallyBounded(s) \\Rightarrow TotallyBounded(s^{-1})$$$

Lean4

@[to_additive]
theorem totallyBounded_inv {s : Set α} (hs : TotallyBounded s) : TotallyBounded (s⁻¹) :=
  by
  convert TotallyBounded.image hs uniformContinuous_inv
  aesop

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