English
Left action distributes over ordinary balls: a • ball b r = ball (a • b) r.
Русский
Левое действие распределяется по обычным шарам: a • ball(b,r) = ball(a•b, r).
LaTeX
$$$\displaystyle a \cdot \mathrm{ball}\,b\,r = \mathrm{ball}\,(a\cdot b)\,r$$$
Lean4
@[to_additive]
theorem smul_ball'' : a • ball b r = ball (a • b) r := by
ext
simp [mem_ball, Set.mem_smul_set, dist_eq_norm_div, _root_.div_eq_inv_mul, ← eq_inv_mul_iff_mul_eq, mul_assoc]