comap_cast_atTop — Mathlib

English

In an Archimedean semiring, the comap of Nat.cast to atTop equals atTop.

Русский

ВArchимедовом полугруппе комап отображения Nat.cast на atTop равен atTop.

LaTeX

$$$[Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] :\quad \operatorname{comap} ( (\uparrow): \mathbb{N} \to R) \operatorname{atTop} = \operatorname{atTop}$$$

Lean4

@[simp]
theorem comap_cast_atTop [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] :
    comap ((↑) : ℕ → R) atTop = atTop :=
  comap_embedding_atTop (fun _ _ => Nat.cast_le) exists_nat_ge

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