closedBall_mono — Mathlib

English

Let p be a seminorm on E. Then for all x ∈ E and r1 ≤ r2, p.closedBall x r1 ⊆ p.closedBall x r2.

Русский

Пусть p — полуправильная норма на E. Тогда для любого x ∈ E и r1 ≤ r2 верно p.closedBall x r1 ⊆ p.closedBall x r2.

LaTeX

$$$\forall x \in E, \forall r_1,r_2 \in \mathbb{R},\ r_1 \le r_2 \Rightarrow p.closedBall x r_1 \subseteq p.closedBall x r_2$$$

Lean4

theorem closedBall_mono {p : Seminorm 𝕜 E} {r₁ r₂ : ℝ} (h : r₁ ≤ r₂) : p.closedBall x r₁ ⊆ p.closedBall x r₂ :=
  fun _ (hx : _ ≤ _) => hx.trans h

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