ball_smul_ball — Mathlib

English

The product of a ball and a ball is contained in a ball of radius the product of the radii: p.ball 0 r1 • p.ball 0 r2 ⊆ p.ball 0 (r1 r2).

Русский

Произведение шара на шар содержится в шар радиуса, равного произведению радиусов: p.ball 0 r1 • p.ball 0 r2 ⊆ p.ball 0 (r1 r2).

LaTeX

$$$p.ball\,0\,r_1 \cdot p.ball\,0\,r_2 \subset p.ball\,0\,(r_1 r_2)$$$

Lean4

theorem ball_smul_ball (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) : Metric.ball (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂) :=
  by
  rcases eq_or_ne r₂ 0 with rfl | hr₂
  · simp
  · exact (smul_subset_smul_left (ball_subset_closedBall _ _ _)).trans (ball_smul_closedBall _ _ hr₂)

Похожие утверждения