hasBasis_smallSets — Mathlib

English

For any filter l on α, l.smallSets has a basis given by membership in l and the powerset operator.

Русский

Для любого фильтра l на α существует базис l.smallSets, задаваемый членством в l и оператором powerset.

LaTeX

$$theorem hasBasis_smallSets (l : Filter α) : HasBasis l.smallSets (fun t : Set α => t ∈ l) Set.powerset$$

Lean4

theorem hasBasis_smallSets (l : Filter α) : HasBasis l.smallSets (fun t : Set α => t ∈ l) powerset :=
  l.basis_sets.smallSets

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