preimage_mul_left_closedBall — Mathlib

English

For a metric group G with isometric left action, nndist(a/b, a/c) = nndist(b,c).

Русский

Для метрогруппы G с изометрическим левым действием выполняется nndist(a/b, a/c) = nndist(b,c).

LaTeX

$$$\operatorname{nndist}(a/b, a/c) = \operatorname{nndist}(b,c)$$$

Lean4

@[to_additive (attr := simp)]
theorem preimage_mul_left_closedBall [IsIsometricSMul G G] (a b : G) (r : ℝ) :
    (a * ·) ⁻¹' closedBall b r = closedBall (a⁻¹ * b) r :=
  preimage_smul_closedBall a b r

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