embeddingUpNat

Mathlib.Algebra.Homology.Embedding.Basic

URI: https://scilib.ai/kg/mathlib#ComplexShape.embeddingUpNat

← MathLib Explorer

English

The embedding from up Nat to up Int satisfies IsRelIff.

Русский

Вложение from up Nat к up Int удовлетворяет IsRelIff.

LaTeX

$$$(ComplexShape.instIsRelIffNatIntEmbeddingUpNat).IsRelIff$$$

Lean4

/-- The obvious embedding from `up ℕ` to `up ℤ`. -/
@[simps!]
def embeddingUpNat : Embedding (up ℕ) (up ℤ) :=
  Embedding.mk' _ _ (fun n => n) (fun _ _ h => by simpa using h) (by dsimp; cutsat)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru