ball_antitone — Mathlib

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

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