closedBall_finset_sup_eq_iInter — Mathlib

English

As above, but for closed balls: closedBall(sup p) x r = ⋂ i ∈ S, closedBall(p i) x r with r ≥ 0.

Русский

Как выше, но для замкнутых шаров: closedBall(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_eq_iInter (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ} (hr : 0 ≤ r) :
    closedBall (s.sup p) x r = ⋂ i ∈ s, closedBall (p i) x r :=
  by
  lift r to NNReal using hr
  simp_rw [closedBall, iInter_setOf, finset_sup_apply, NNReal.coe_le_coe, Finset.sup_le_iff, ← NNReal.coe_le_coe,
    NNReal.coe_mk]

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