tendsto_intCast_atTop_atTop — Mathlib

English

The natural embedding of integers into any Archimedean ordered ring is topologically cofinal: sending ℤ into R preserves the atTop limit.

Русский

Естественное вложение целых чисел в Archimedean упорядоченное кольцо является топологически кограничным: отображение ℤ в R сохраняет предел atTop.

LaTeX

$$$\operatorname{Tendsto}((\uparrow) : \mathbb{Z} \to R)\ \mathrm{atTop} \ \mathrm{atTop}$$$

Lean4

theorem tendsto_intCast_atTop_atTop [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] :
    Tendsto ((↑) : ℤ → R) atTop atTop :=
  tendsto_intCast_atTop_iff.2 tendsto_id

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