Theorems · Theorem · order theory

Finset.swap_mem_addAntidiagonal

Deprecated since 2026-06-08Use Finset.swap_mem_antidiagonal instead.

∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α},
  x.swap ∈ Finset.antidiagonal hs ht a ↔ x ∈ Finset.antidiagonal ht hs a

Alias of Finset.swap_mem_antidiagonal.

Defined in

Mathlib.Data.Finset.MulAntidiagonal

Cited by

0 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidPartialOrderIsOrderedCancelAddMonoid