to_nat_inj

Mathlib.Data.Num.Lemmas

URI: https://scilib.ai/kg/mathlib#PosNum.to_nat_inj

← MathLib Explorer

English

The natural embedding of PosNum into ℕ is injective: (m : ℕ) = n implies m = n.

Русский

Естественное вложение PosNum в ℕ инъективно: (m : ℕ) = n ⇒ m = n.

LaTeX

$$$ (m : \mathbb{N}) = n \iff m = n $$$

Lean4

@[norm_cast]
theorem to_nat_inj {m n : PosNum} : (m : ℕ) = n ↔ m = n :=
  ⟨fun h => Num.pos.inj <| by rw [← PosNum.of_to_nat, ← PosNum.of_to_nat, h], congr_arg _⟩

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

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

Разделы

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

Аффилиация

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