comap_cast_atTop — Mathlib

English

For a ring R with Archimedean property, comap of Int.cast to atTop equals atTop.

Русский

Для кольца R с свойством Archimedean comap Int.cast к atTop равен atTop.

LaTeX

$$$[Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R]\; :\; \operatorname{comap} (\text{Int.cast}) \operatorname{Filter.atTop} = \operatorname{Filter.atTop}$$$

Lean4

@[simp]
theorem comap_cast_atTop [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] :
    comap ((↑) : ℤ → R) atTop = atTop :=
  comap_embedding_atTop (fun _ _ => Int.cast_le) fun r =>
    let ⟨n, hn⟩ := exists_nat_ge r;
    ⟨n, mod_cast hn⟩

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