smul_closedBall — Mathlib

English

For any c ∈ G, the image of a closed ball under the action by c is the closed ball around c • x with the same radius: c • closedBall(x,r) = closedBall(c • x, r).

Русский

Для любого c ∈ G образ закрытого шара под действием c — это закрытый шар вокруг c • x с тем же радиусом.

LaTeX

$$$c\cdot \overline{\mathrm{Ball}}(x,r) = \overline{\mathrm{Ball}}(c\cdot x, r)$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_closedBall (c : G) (x : X) (r : ℝ≥0∞) : c • closedBall x r = closedBall (c • x) r :=
  (IsometryEquiv.constSMul c).image_emetric_closedBall _ _

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