pair_eq_pair — Mathlib

English

Two natural number pairs map to the same natural via pairing iff their components are equal.

Русский

Две пары чисел дают один и тот же код через кодирование пары тогда и только тогда, когда их координаты совпадают.

LaTeX

$$$ \forall a,b,c,d \in \mathbb{N}, \; \operatorname{pair} a b = \operatorname{pair} c d \iff a=c \land b=d. $$$

Lean4

@[simp]
theorem pair_eq_pair {a b c d : ℕ} : pair a b = pair c d ↔ a = c ∧ b = d :=
  pairEquiv.injective.eq_iff.trans (@Prod.ext_iff ℕ ℕ (a, b) (c, d))

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