smallSets — Mathlib

English

If l has a basis p s, then l.smallSets has basis p with the family of sets being the powerset of s(i).

Русский

Если у фильтра l есть база p s, то l.smallSets имеет базис p и семейство множест s(i).powerset.

LaTeX

$$HasBasis l p s → HasBasis l.smallSets p fun i => 𝒫 s i$$

Lean4

protected theorem smallSets {p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) :
    HasBasis l.smallSets p fun i => 𝒫 s i :=
  h.lift' monotone_powerset

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