basisSets_univ_mem — Mathlib

English

The universal set is contained in the basis of p, i.e., the basis includes the whole space as a basis element.

Русский

Универсум содержится в базисе p; база включает всё пространство как элемент базиса.

LaTeX

$$univ \in p.basisSets$$

Lean4

theorem basisSets_univ_mem : univ ∈ p.basisSets :=
  (basisSets_iff _).mpr ⟨∅, _, one_pos, by rw [Finset.sup_empty, Seminorm.bot_eq_zero, ball_zero' _ one_pos]⟩

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