instSupSet — Mathlib

English

The supremum of a family S of filters on α is the intersection of all filters in S; equivalently, s ∈ sSup S iff ∀ f ∈ S, s ∈ f.

Русский

Супремум семейства фильтров S на α равен пересечению всех фильтров из S; то есть s ∈ sSup S тогда и только тогда, когда ∀ f ∈ S, s ∈ f.

LaTeX

$$$\\operatorname{sSup} S = \\bigcap_{f \\in S} f, \\quad s \\in \\operatorname{sSup} S \\iff \\forall f \\in S, s \\in f$$$

Lean4

instance instSupSet : SupSet (Filter α) where sSup S := join (𝓟 S)

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