pair_eq_of_unpair_eq

Mathlib.Data.Nat.Pairing

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

English

If unpair n equals (a,b), then the pair a b equals n.

Русский

Если unpair n = (a,b), то pair a b = n.

LaTeX

$$$ \forall {n\ a\ b}, \; (\operatorname{unpair} n = (a,b)) \rightarrow \operatorname{pair} a b = n. $$$

Lean4

theorem pair_eq_of_unpair_eq {n a b} (H : unpair n = (a, b)) : pair a b = n := by simpa [H] using pair_unpair n

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

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

Разделы

Аффилиация

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