English
If r1 ≠ 0, then scaling the 𝕜-ball of radius r1 by every element of p.ball 0 r2 yields a subset of the (Euclidean) ball of radius r1 r2 around 0 under p.
Русский
Если r1 ≠ 0, масштабирование 𝕜-шара радиуса r1 по любой точке из p.ball 0 r2 вложено в шар радиуса r1 r2 вокруг 0 для p.
LaTeX
$$$r_1 \neq 0 \Rightarrow \mathrm{Metric.closedBall}(0,r_1) \cdot p.ball(0,r_2) \subset p.ball(0,r_1 r_2)$$$
Lean4
theorem closedBall_smul_ball (p : Seminorm 𝕜 E) {r₁ : ℝ} (hr₁ : r₁ ≠ 0) (r₂ : ℝ) :
Metric.closedBall (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂) :=
by
simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero_iff, map_smul_eq_mul]
refine fun a ha b hb ↦ mul_lt_mul' ha hb (apply_nonneg _ _) ?_
exact hr₁.lt_or_gt.resolve_left <| ((norm_nonneg a).trans ha).not_gt
