English
The ball under the norm of k scales by |k|: the ball p around 0 with radius ||k||·r contains the k-scaling of the ball of radius r.
Русский
Шар по норме масштабается по модулю k: шар p вокруг 0 радиуса ||k||·r содержит k-умножение шара радиуса r.
LaTeX
$$$p.ball(0,\|k\|\,r) \supseteq k \cdot p.ball(0,r)$$$
Lean4
theorem ball_norm_mul_subset {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} : p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r :=
by
rcases eq_or_ne k 0 with (rfl | hk)
· rw [norm_zero, zero_mul, ball_eq_emptyset _ le_rfl]
exact empty_subset _
· intro x
rw [Set.mem_smul_set, Seminorm.mem_ball_zero]
refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩
·
rwa [Seminorm.mem_ball_zero, map_smul_eq_mul, norm_inv, ← mul_lt_mul_iff_right₀ <| norm_pos_iff.mpr hk, ←
mul_assoc, ← div_eq_mul_inv ‖k‖ ‖k‖, div_self (ne_of_gt <| norm_pos_iff.mpr hk), one_mul]
rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self hk, one_smul]
