instTop — Mathlib

English

The top filter on α is the largest filter, obtained as the supremum of all principal filters and equivalently consists of the sets that contain every element of α (i.e., only univ).

Русский

Верхний фильтр на α является наибольшим фильтром; он достигается как супремум всех принципиальных фильтров и эквивалентно состоит из множеств, содержащих каждый элемент α (то есть только univ).

LaTeX

$$$\\mathrm{Top}(\\mathrm{Filter}(\\alpha)) = \\mathrm{sSup}(\\{\\mathrm{pure}(a) \\mid a \\in \\alpha\\})$$$

Lean4

instance : Top (Filter α) where top := .copy (sSup (Set.range pure)) {s | ∀ x, x ∈ s} <| by simp

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