smul_ball'' — Mathlib

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]

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