ball_zero' — Mathlib

English

For a finite nonempty index set, the ball of the supremum seminorm equals the infimum of the balls for each index: ball (s.sup' H p) e r = s.inf' H (i ↦ (p i).ball e r).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem ball_zero' (x : E) (hr : 0 < r) : ball (0 : Seminorm 𝕜 E) x r = Set.univ :=
  by
  rw [Set.eq_univ_iff_forall, ball]
  simp [hr]

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