succ_injective

Mathlib.Data.Nat.Basic

URI: https://scilib.ai/kg/mathlib#Nat.succ_injective

English

The successor function on natural numbers is injective: if a+1 = b+1 then a = b.

Русский

Функция successor на натуральных числах инъективна: если a+1 = b+1, то a = b.

LaTeX

$$$\forall a,b \in \mathbb{N}, \; \operatorname{succ}(a) = \operatorname{succ}(b) \Rightarrow a=b$$$

Lean4

theorem succ_injective : Injective Nat.succ :=
  @succ.inj

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

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

Разделы

Аффилиация

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