English
Let p be a seminorm on a vector space E. Then for every x ∈ E and radii r1, r2 ∈ R with r1 ≤ r2, the ball of radius r1 around x is contained in the ball of radius r2 around x: p.ball x r1 ⊆ p.ball x r2.
Русский
Пусть p — полуправильная норма (семинормa) на векторном пространстве E. Тогда для любого x ∈ E и радиусов r1, r2 ∈ R с r1 ≤ r2 шар p вокруг x радиуса r1 содержится в шаре p вокруг x радиуса r2: p.ball x r1 ⊆ p.ball x r2.
LaTeX
$$$\forall x \in E, \forall r_1,r_2 \in \mathbb{R},\ r_1 \le r_2 \Rightarrow p.ball x r_1 \subseteq p.ball x r_2$$$
Lean4
theorem ball_mono {p : Seminorm 𝕜 E} {r₁ r₂ : ℝ} (h : r₁ ≤ r₂) : p.ball x r₁ ⊆ p.ball x r₂ := fun _ (hx : _ < _) =>
hx.trans_le h
