surjective_unpair

Mathlib.Data.Nat.Pairing

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

English

The unpair function is surjective: every pair of natural numbers (a,b) occurs as unpair(n) for some n.

Русский

Функция распаковки сюръективна: для любой пары (a,b) найдётся n such that unpair(n) = (a,b).

LaTeX

$$$ \forall a,b \in \mathbb{N}, \; \exists n \in \mathbb{N}, \; \operatorname{unpair}(n) = (a,b). $$$

Lean4

theorem surjective_unpair : Surjective unpair :=
  pairEquiv.symm.surjective

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

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

Разделы

Аффилиация

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