instInfSet — Mathlib

English

The InfSet structure on the family of filters is realized by taking the infimum operation to be Filter.sInf.

Русский

Структура InfSet на множестве фильтров реализуется через взятие бесконечного нижнего предела — это Filter.sInf.

LaTeX

$$$\\text{InfSet}(\\text{Filter}(\\alpha)):\\; S \\mapsto \\operatorname{sInf}(S) \\quad\\text{with}\\quad \\operatorname{sInf}(S) = \\operatorname{Filter.sInf}(S).$$$

Lean4

instance instInfSet : InfSet (Filter α) where sInf := Filter.sInf

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