atTop_basis — Mathlib

English

The atTop filter has an antitone basis given by the sets {x ∈ α | a ≤ x} (Ici) for a directed preorder with a nonempty index set.

Русский

У фильтра atTop есть антиинкрементальный базис, задаваемый множествами {x ∈ α | a ≤ x} (Ici) для направленного предела с непустым индексным набором.

LaTeX

$$$ \\text{HasAntitoneBasis}(\\operatorname{atTop}, \\mathbf{Ici}) $$$

Lean4

theorem atTop_basis [Nonempty α] : (@atTop α _).HasBasis (fun _ => True) Ici :=
  hasAntitoneBasis_atTop.1

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