preimage_smul_closedBall — Mathlib

English

The preimage of a closedBall under the smul action equals the closedBall around c^{-1}•x with the same radius: (c•·)^{-1} closedBall(x,r) = closedBall(c^{-1}•x, r).

Русский

Предобраз замкнутого шара под действием smul равен замкнутому шару вокруг c^{-1}•x с тем же радиусом.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem preimage_smul_closedBall (c : G) (x : X) (r : ℝ) : (c • ·) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r := by
  rw [preimage_smul, smul_closedBall]

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