preimage_mul_right_ball — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem preimage_mul_right_ball [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ) :
    (fun x => x * a) ⁻¹' ball b r = ball (b / a) r :=
  by
  rw [div_eq_mul_inv]
  exact preimage_smul_ball (MulOpposite.op a) b r

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