swap_mem_mulAntidiagonal — Mathlib

English

Swapping the factors preserves membership in the corresponding antidiagonal sets: x.swap ∈ mulAntidiagonal hs ht a iff x ∈ mulAntidiagonal ht hs a.

Русский

Замена местами факторов сохраняет принадлежность к соответствующим множествам антидиагонали: x.swap ∈ mulAntidiagonal hs ht a ⇔ x ∈ mulAntidiagonal ht hs a.

LaTeX

$$x.swap ∈ mulAntidiagonal hs ht a ↔ x ∈ mulAntidiagonal ht hs a$$

Lean4

@[to_additive]
theorem swap_mem_mulAntidiagonal : x.swap ∈ Finset.mulAntidiagonal hs ht a ↔ x ∈ Finset.mulAntidiagonal ht hs a := by
  simp

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