English
For a seminorm p on E and vectors x1, x2 ∈ E with radii r1, r2 ∈ R, the Minkowski sum of the balls satisfies p.ball x1 r1 + p.ball x2 r2 ⊆ p.ball (x1 + x2) (r1 + r2).
Русский
Для полунормы p на E и векторов x1, x2 ∈ E с радиусами r1, r2 ∈ R выполняется: p.ball x1 r1 + p.ball x2 r2 ⊆ p.ball (x1 + x2) (r1 + r2).
LaTeX
$$$\forall x_1, x_2 \in E, \forall r_1, r_2 \in \mathbb{R},\ p.ball(x_1,r_1) + p.ball(x_2,r_2) \subseteq p.ball(x_1+x_2, r_1+r_2)$$$
Lean4
theorem ball_add_ball_subset (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) (x₁ x₂ : E) :
p.ball (x₁ : E) r₁ + p.ball (x₂ : E) r₂ ⊆ p.ball (x₁ + x₂) (r₁ + r₂) :=
by
rintro x ⟨y₁, hy₁, y₂, hy₂, rfl⟩
rw [mem_ball, add_sub_add_comm]
exact (map_add_le_add p _ _).trans_lt (add_lt_add hy₁ hy₂)
