embeddingUpIntGE — Mathlib

English

The map n ↦ p+n defines an embedding from up ℕ to up ℤ, preserving the relational structure between indices, i.e., it is an isomorphism of the index relations.

Русский

Отображение n ↦ p+n задаёт вложение from up ℕ в up ℤ, сохраняющее отношение между индексами, то есть оно является изоморфизмом отношений между индексами.

LaTeX

$$$\\text{embeddingUpIntGE}(p):\\mathrm{Embedding}(\\mathrm{up}\\mathbb{N})(\\mathrm{up}\\mathbb{Z}),\\quad f(n)=p+n$$$

Lean4

/-- The embedding from `up ℕ` to `up ℤ` which sends `n : ℕ` to `p + n`. -/
@[simps!]
def embeddingUpIntGE : Embedding (up ℕ) (up ℤ) :=
  Embedding.mk' _ _ (fun n => p + n) (fun _ _ h => by dsimp at h; cutsat) (by dsimp; cutsat)

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