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