atBot_countable_basis — Mathlib

English

There exists a countable basis for the atBot filter on α with the appropriate directedness.

Русский

Существует счётная база для фильтра atBot над α.

LaTeX

$$$$\text{HasCountableBasis}(\operatorname{atBot}_{\alpha}, \text{True}, \mathbf{Iic}).$$$$

Lean4

theorem atBot_countable_basis [Preorder α] [IsDirected α (· ≥ ·)] [Nonempty α] [Countable α] :
    HasCountableBasis (atBot : Filter α) (fun _ => True) Iic :=
  { atBot_basis with countable := to_countable _ }

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