iSup_sets_eq — Mathlib

English

The index-wise supremum of a family of filters has its sets equal to the intersection of the sets of all indexed filters.

Русский

Предел по индексу iSup для семейства фильтров имеет множества, равные пересечению множеств всех фильтров по индексу.

LaTeX

$$$(\\mathrm{iSup} f).\\text{sets} = \\bigcap_{i} (f(i)).\\text{sets}$$$

Lean4

theorem iSup_sets_eq {f : ι → Filter α} : (iSup f).sets = ⋂ i, (f i).sets :=
  (giGenerate α).gc.u_iInf

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