closedBall_zero' — Mathlib

English

For a nonempty finite index set, the closedBall of the supremum equals the infimum of the individual closedBalls: closedBall (s.sup' H p) e r = s.inf' H (i ↦ closedBall (p i) e r).

Русский

Для непустого конечного множества индексов замкнутый шар над супремумом равен инфимуму замкнутых шаров по каждому индексу.

LaTeX

$$$\\mathrm{closedBall}_{s.sup' H p}(e,r) = \\inf' H\\; (i \\mapsto \\mathrm{closedBall}_{p_i}(e,r))$$$

Lean4

@[simp]
theorem closedBall_zero' (x : E) (hr : 0 < r) : closedBall (0 : Seminorm 𝕜 E) x r = Set.univ :=
  eq_univ_of_subset (ball_subset_closedBall _ _ _) (ball_zero' x hr)

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