toNat_injective

Mathlib.Data.Num.Lemmas

URI: https://scilib.ai/kg/mathlib#Num.toNat_injective

English

The cast from Num to natural numbers is injective: if m and n have the same nat-cast, then m = n.

Русский

Отображение Num в ℕ инъективно: если m и n имеют одинаковое отображение в ℕ, то m = n.

LaTeX

$$$\\forall m,n : Num, (m : \\mathbb{N}) = (n : \\mathbb{N}) \\Rightarrow m = n$$$

Lean4

theorem toNat_injective : Function.Injective (castNum : Num → ℕ) :=
  Function.LeftInverse.injective of_to_nat'

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

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

Разделы

Аффилиация

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