English
Let R be a ring endowed with a compatible partial order and Archimedean property, and consider the natural embedding of the integers into R. Then pulling back the bottom filter along this embedding yields the bottom filter again.
Русский
Пусть R — кольцо с совместимым частичным порядком и свойством Архимедовости; пусть существует естественное вложение целых чисел в R. Тогда обратное отображение нижнего фильтра по этому вложению равно нижнему фильтру.
LaTeX
$$$\operatorname{comap}((\uparrow) : \mathbb{Z} \to R) \ \mathrm{atBot} = \mathrm{atBot}$$$
Lean4
@[simp]
theorem comap_cast_atBot [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] :
comap ((↑) : ℤ → R) atBot = atBot :=
comap_embedding_atBot (fun _ _ => Int.cast_le) fun r =>
let ⟨n, hn⟩ := exists_nat_ge (-r)
⟨-n, by simpa [neg_le] using hn⟩
