English
A variant of smul for closedBalls: the smul of a closedBall by k scales radius by ||k||.
Русский
Вариант умножения замкнутого шара: умножение на k масштабирует радиус на ||k||.
LaTeX
$$$k \cdot (p.closedBall(0,r)) = p.closedBall(0,\|k\| r)$$$
Lean4
theorem smul_closedBall_zero {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} (hk : 0 < ‖k‖) :
k • p.closedBall 0 r = p.closedBall 0 (‖k‖ * r) :=
by
refine subset_antisymm smul_closedBall_subset ?_
intro x
rw [Set.mem_smul_set, Seminorm.mem_closedBall_zero]
refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩
· rwa [Seminorm.mem_closedBall_zero, map_smul_eq_mul, norm_inv, inv_mul_le_iff₀ hk]
rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self (norm_pos_iff.mp hk), one_smul]
