atTop_hasCountableBasis_of_archimedean

English

There is a countable basis for the atTop filter in archimedean settings, with sets of the form Ici n.

Русский

В условиях Архимедова предела имеется счетный базис для фильтра atTop в виде множеств $[n, \infty)$.

LaTeX

$$$(\mathrm{atTop} : \mathrm{Filter}\, R).\mathrm{HasCountableBasis} (\lambda _ : \mathbb{N},\; \mathrm{Ici}\,\text{_})\ changed$$

Lean4

theorem atTop_hasCountableBasis_of_archimedean [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
    (atTop : Filter R).HasCountableBasis (fun _ : ℕ => True) fun n => Ici n :=
  ⟨atTop_hasAntitoneBasis_of_archimedean.1, to_countable _⟩

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