comap_cast_atTop — Mathlib

English

The embedding of rational numbers into any Archimedean ordered ring preserves the atTop filter via comap.

Русский

Встраивание рациональных чисел в Archimedeанское упорядоченное кольцо сохраняет фильтр atTop через произведение обратного отображения.

LaTeX

$$$\operatorname{comap}((\uparrow) : \mathbb{Q} \to R) \ \mathrm{atTop} = \mathrm{atTop}$$$

Lean4

@[simp]
theorem comap_cast_atTop [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] :
    comap ((↑) : ℚ → R) atTop = atTop :=
  comap_embedding_atTop (fun _ _ => Rat.cast_le) fun r =>
    let ⟨n, hn⟩ := exists_nat_ge r;
    ⟨n, by simpa⟩

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