smul_ball — Mathlib

English

If the action is isometric, then the image of a ball under the group action is a ball with the same radius around the translated center: c • Ball(x,r) = Ball(c • x, r).

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem smul_ball (c : G) (x : X) (r : ℝ) : c • ball x r = ball (c • x) r :=
  (IsometryEquiv.constSMul c).image_ball _ _

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