closedBall_antitone — Mathlib

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

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