ball_finset_sup — Mathlib

English

Same as Ball Finset Sup: ball(s.sup p) x r = ⋂ i ∈ S, ball(p i) x r for r > 0.

Русский

То же самое, что и Ball Finset Sup: ball(s.sup p) x r = ⋂ i ∈ S, ball(p i) x r при r > 0.

LaTeX

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

Lean4

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

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