smul_ball — Mathlib

English

In the extended metric space setting, for any c ∈ G and x ∈ X and r ≥ 0, the image of the ball by the action is the ball around the moved point: c • Ball(x,r) = Ball(c • x, r).

Русский

В рамках расширенного метрического пространства образ шара под действием c • — это шар вокруг точки c • x: 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 : ℝ≥0∞) : c • ball x r = ball (c • x) r :=
  (IsometryEquiv.constSMul c).image_emetric_ball _ _

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