inv_closedBall — Mathlib

English

Let E be a seminormed commutative group. The inverse map sends a closed ball around x of radius δ to the closed ball around x^{-1} of the same radius: (closedBall(x, δ))^{-1} = closedBall(x^{-1}, δ).

Русский

Пусть E — полугруппа с полунормой, коммутативная. Обратное отображение переводит замкнутый шар окружности δ с центром x в замкнутый шар с центром x^{-1} той же радиуса: (closedBall(x, δ))^{-1} = closedBall(x^{-1}, δ).

LaTeX

$$$$(\overline{B}(x,\delta))^{-1} = \overline{B}(x^{-1}, \delta)$$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_closedBall : (closedBall x δ)⁻¹ = closedBall x⁻¹ δ :=
  (IsometryEquiv.inv E).preimage_closedBall x δ

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