closedBall_sup — Mathlib

English

The closedBall of the supremum of two seminorms equals the intersection of the individual closedBalls: closedBall(p ⊔ q) e r = closedBall(p) e r ∩ closedBall(q) e r.

Русский

Замкнутый шар над максимумом полиномона равен пересечению замкнутых шаров по каждому полиномону.

LaTeX

$$$\\mathrm{closedBall}_{p \\sqcup q}(e,r) = \\mathrm{closedBall}_p(e,r) \\cap \\mathrm{closedBall}_q(e,r)$$$

Lean4

theorem closedBall_sup (p : Seminorm 𝕜 E) (q : Seminorm 𝕜 E) (e : E) (r : ℝ) :
    closedBall (p ⊔ q) e r = closedBall p e r ∩ closedBall q e r := by
  simp_rw [closedBall, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_le_iff]

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