sSup_sets_eq — Mathlib

English

The supremum over a set S of filters has its sets equal to the intersection over all filters in S.

Русский

Предел над множеством фильтров S имеет множества, равные пересечению множеств всех фильтров в S.

LaTeX

$$$(\\mathrm{sSup}(S)).\\text{sets} = \\bigcap_{f \\in S} (f:\\mathrm{Filter}(\\alpha)).\\text{sets}$$$

Lean4

theorem sSup_sets_eq {s : Set (Filter α)} : (sSup s).sets = ⋂ f ∈ s, (f : Filter α).sets :=
  (giGenerate α).gc.u_sInf

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