ball_finset_sup_eq_iInter — Mathlib

English

Let p : ι → Seminorm 𝕜 E; S finite; x ∈ E; r > 0. Then ball(sup p) x r equals the infimum over i ∈ S of the balls ball(p i) x r.

Русский

Пусть p : ι → Seminorm 𝕜 E; S конечен; x ∈ E; r > 0. Тогда ball(sup p) x r равно пересечению шаров, т.е. инф по i ∈ S от ball(p i) x r.

LaTeX

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

Lean4

theorem ball_finset_sup_eq_iInter (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ} (hr : 0 < r) :
    ball (s.sup p) x r = ⋂ i ∈ s, ball (p i) x r :=
  by
  lift r to NNReal using hr.le
  simp_rw [ball, iInter_setOf, finset_sup_apply, NNReal.coe_lt_coe, Finset.sup_lt_iff (show ⊥ < r from hr), ←
    NNReal.coe_lt_coe, NNReal.coe_mk]

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