antidiagonal_congr' — Mathlib

English

A variant of the congruence principle for antidiagonal elements shows equality is governed by the second coordinate when viewed under a swapping symmetry.

Русский

Вариант принципа согласования антидиагоналей: равенство определяется второй координатой с учётом симметрии обмена.

LaTeX

$$$p=q \\iff p.2 = q.2 \\quad (p,q \\in \\operatorname{antidiagonal}(n))$$$

Lean4

/-- A point in the antidiagonal is determined by its second coordinate.

See also `Finset.antidiagonal_congr`. -/
theorem antidiagonal_congr' (hp : p ∈ antidiagonal n) (hq : q ∈ antidiagonal n) : p = q ↔ p.2 = q.2 :=
  by
  rw [← Prod.swap_inj]
  exact antidiagonal_congr (swap_mem_antidiagonal.2 hp) (swap_mem_antidiagonal.2 hq)

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