swap_mem_antidiagonal — Mathlib

English

Swapping the coordinates of a pair in the antidiagonal preserves membership: xy.swap ∈ antidiagonal(n) iff xy ∈ antidiagonal(n).

Русский

Обмен координат в паре антидиагонали сохраняет принадлежность: xy.swap ∈ antidiagonal(n) тогда и только тогда, когда xy ∈ antidiagonal(n).

LaTeX

$$$\\mathrm{xy.swap} \\in \\operatorname{antidiagonal}(n) \\iff xy \\in \\operatorname{antidiagonal}(n)$$$

Lean4

theorem swap_mem_antidiagonal [AddCommMonoid A] [HasAntidiagonal A] {n : A} {xy : A × A} :
    xy.swap ∈ antidiagonal n ↔ xy ∈ antidiagonal n := by simp [add_comm]

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