atTop_countable_basis — Mathlib

English

There exists a countable basis for the atTop filter on α, for suitable τ (e.g., directed, nonempty, countable).

Русский

Существуют счётные базисные множества для фильтра atTop на α.

LaTeX

$$$$\text{HasCountableBasis}(\operatorname{atTop}_{\alpha}, \text{True}, \mathbf{Icc}()).$$$$

Lean4

theorem atTop_countable_basis [Preorder α] [IsDirected α (· ≤ ·)] [Nonempty α] [Countable α] :
    HasCountableBasis (atTop : Filter α) (fun _ => True) Ici :=
  { atTop_basis with countable := to_countable _ }

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