atTop_hasAntitoneBasis_of_archimedean

English

The atTop filter on any Archimedean ordered semiring has a countable antitone basis given by the sets Ici n, via natural cast.

Русский

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

LaTeX

$$$(\,\text{atTop} : \mathrm{Filter}\, R).\mathrm{HasAntitoneBasis} (\lambda n: \mathbb{N},\; \mathrm{Ici}\,n)$$$

Lean4

theorem atTop_hasAntitoneBasis_of_archimedean [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
    (atTop : Filter R).HasAntitoneBasis fun n : ℕ => Ici n :=
  hasAntitoneBasis_atTop.comp_mono Nat.mono_cast tendsto_natCast_atTop_atTop

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