smul_closedBall — Mathlib

English

Under an isometric action, the image of a closed ball is the closed ball around the translated center with the same radius: c • closedBall(x,r) = closedBall(c • x, r).

Русский

При изометрическом действии образ замкнутого шара есть замкнутый шар с тем же радиусом вокруг перенесённого центра: c•closedBall(x,r) = closedBall(c•x, r).

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 : ℝ) : c • closedBall x r = closedBall (c • x) r :=
  (IsometryEquiv.constSMul c).image_closedBall _ _

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