English
Let p and q be seminorms on E with q ≤ p. Then for every x ∈ E and r ∈ R, p.closedBall x r ⊆ q.closedBall x r.
Русский
Пусть p и q — семинормы на E и q ≤ p. Тогда для любого x ∈ E и r ∈ R верно p.closedBall x r ⊆ q.closedBall x r.
LaTeX
$$$\forall x \in E, \forall r \in \mathbb{R},\ p.closedBall x r \subseteq q.closedBall x r\quad \text{при } q \le p$$$
Lean4
theorem closedBall_antitone {p q : Seminorm 𝕜 E} (h : q ≤ p) : p.closedBall x r ⊆ q.closedBall x r := fun _ =>
(h _).trans