English
Two antidiagonal elements are equal if and only if their first coordinates match; this gives a coordinate-determined equality principle for antidiagonal pairs.
Русский
Два элемента антидиагонали равны тогда и только тогда, когда их первые координаты совпадают; это даёт принцип равенства пар антидиагонали, определяемый координатами.
LaTeX
$$$p=q \\iff p.1 = q.1 \\quad (p,q \\in \\operatorname{antidiagonal}(n))$$$
Lean4
/-- A point in the antidiagonal is determined by its first coordinate.
See also `Finset.antidiagonal_congr'`. -/
theorem antidiagonal_congr (hp : p ∈ antidiagonal n) (hq : q ∈ antidiagonal n) : p = q ↔ p.1 = q.1 :=
by
refine ⟨congr_arg Prod.fst, fun h ↦ Prod.ext h ((add_right_inj q.fst).mp ?_)⟩
rw [mem_antidiagonal] at hp hq
rw [hq, ← h, hp]
