closedBall_finset_sup — Mathlib

English

Same as above for closed balls with nonnegative radius: closedBall(s.sup p) x r = ⋂ i ∈ S, closedBall(p i) x r if r ≥ 0.

Русский

То же самое для замкнутых шаров: closedBall(s.sup p) x r = ⋂ i ∈ S, closedBall(p i) x r при r ≥ 0.

LaTeX

$$$\text{closedBall}(\,s.sup p\,)\,x\,r = \bigcap_{i \in s} \text{closedBall}(p i)\,x\,r$$$

Lean4

theorem closedBall_finset_sup (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ} (hr : 0 ≤ r) :
    closedBall (s.sup p) x r = s.inf fun i => closedBall (p i) x r :=
  by
  rw [Finset.inf_eq_iInf]
  exact closedBall_finset_sup_eq_iInter _ _ _ hr

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