English
The product of a closed ball with a closed ball is contained in a closed ball with radius the product of the radii: Metric.closedBall(0,r1) • p.closedBall 0 r2 ⊆ p.closedBall 0 (r1 r2).
Русский
Произведение двух замкнутых шаров вложено в замкнутый шар радиуса r1 r2: Metric.closedBall(0,r1) • p.closedBall 0 r2 ⊆ p.closedBall 0 (r1 r2).
LaTeX
$$$\text{Metric.closedBall}(0,r_1) \cdot p.closedBall(0,r_2) \subset p.closedBall(0,(r_1 r_2))$$$
Lean4
theorem closedBall_smul_closedBall (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
Metric.closedBall (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂) :=
by
simp only [smul_subset_iff, mem_closedBall_zero, mem_closedBall_zero_iff, map_smul_eq_mul]
intro a ha b hb
gcongr
exact (norm_nonneg _).trans ha
