basisSets_mem — Mathlib

English

Characterizes basisSets: a set U is in basisSets iff U equals a ball around 0 with radius r for some finite supremum of seminorms.

Русский

Характеризуется принадлежность множества basisSets: U принадлежит basisSets тогда и только тогда, когда U равно шаре вокруг 0 радиуса r для некоторого конечного супа семинормов.

LaTeX

$$theorem basisSets_iff {U : Set E} : U ∈ p.basisSets ↔ ∃ (i : Finset ι) (r : ℝ), 0 < r ∧ U = ball (i.sup p) 0 r$$

Lean4

theorem basisSets_mem (i : Finset ι) {r : ℝ} (hr : 0 < r) : (i.sup p).ball 0 r ∈ p.basisSets :=
  (basisSets_iff _).mpr ⟨i, _, hr, rfl⟩

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