English
The smul of a 𝕜-ball with a p-ball around 0 is contained in a ball around 0 with radius the product of the radii: (β-ball) • (closedBall) ⊆ ball with product radius.
Русский
Умножение шара 𝕜 на замкнутый шар вокруг 0 вложено в шар вокруг 0 радиуса равного произведению радиусов.
LaTeX
$$$p.ball\,0\,r_1\cdot (p.closedBall\,0\,r_2) \subset p.ball\,0\,(r_1 r_2)$$$
Lean4
theorem ball_smul_closedBall (p : Seminorm 𝕜 E) (r₁ : ℝ) {r₂ : ℝ} (hr₂ : r₂ ≠ 0) :
Metric.ball (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.ball 0 (r₁ * r₂) :=
by
simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero, mem_ball_zero_iff, map_smul_eq_mul]
intro a ha b hb
rw [mul_comm, mul_comm r₁]
refine mul_lt_mul' hb ha (norm_nonneg _) (hr₂.lt_or_gt.resolve_left ?_)
exact ((apply_nonneg p b).trans hb).not_gt
