smallSets — Mathlib

English

For a filter l on α, the smallSets filter on Set α is the lift of powerset along l; i.e., it is the largest filter on Set α containing all powersets of members of l.

Русский

Для фильтра l на α фильтр smallSets над Set α есть lift по powerset; то есть он является наибольшим фильтром на Set α, содержащим множества вида powerset(S) для S ∈ l.

LaTeX

$$$\operatorname{smallSets}(l) = l.{\mathrm{lift}'}(\mathrm{powerset})$$$

Lean4

/-- The filter `l.smallSets` is the largest filter containing all powersets of members of `l`. -/
def smallSets (l : Filter α) : Filter (Set α) :=
  l.lift' powerset

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