basisSets_singleton_mem — Mathlib

English

Let p be a SeminormFamily on E. For every index i and every radius r > 0, the ball centered at 0 with radius r defined by p_i is a member of the basis of seminorm neighborhoods.

Русский

Пусть p — семейство полумер полусходов на E. Для любого индекса i и любого радиуса r > 0 шар, центрированный в нуле, радиуса r, определяемый p_i, принадлежит базису окрестностей полусеминорм.

LaTeX

$$$\forall i:\iota,\forall r>0:\ (p\,i).ball\ 0\ r \in p.basisSets$$$

Lean4

theorem basisSets_singleton_mem (i : ι) {r : ℝ} (hr : 0 < r) : (p i).ball 0 r ∈ p.basisSets :=
  (basisSets_iff _).mpr ⟨{ i }, _, hr, by rw [Finset.sup_singleton]⟩

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