smul_closedBall'' — Mathlib

English

Multiplication by a scalar on the left distributes over closed balls: a • closedBall b r = closedBall (a • b) r.

Русский

Смещение на лево через скаляр распределяется по закрытым шарам: a • closedBall(b,r) = closedBall(a•b, r).

LaTeX

$$$\displaystyle a \cdot \mathrm{closedBall}\,b\,r = \mathrm{closedBall}\,(a\cdot b)\,r$$$

Lean4

@[to_additive]
theorem smul_closedBall'' : a • closedBall b r = closedBall (a • b) r :=
  by
  ext
  simp [mem_closedBall, Set.mem_smul_set, dist_eq_norm_div, div_eq_inv_mul, ← eq_inv_mul_iff_mul_eq, mul_assoc]

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