Theorems · Definition · order theory

Finset.antidiagonal

{α : Type u_1} →
  [inst : AddCommMonoid α] →
    [inst_1 : PartialOrder α] → [IsOrderedCancelAddMonoid α] → {s t : Set α} → s.IsPWO → t.IsPWO → α → Finset (α × α)

Finset.antidiagonal hs ht a is the set of all pairs of an element in s and an element in t that add to a, but its construction requires proofs that s and t are well-ordered.

Defined in

Mathlib.Data.Finset.MulAntidiagonal

Cited by

23 results in Mathlib

Foundations

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

Assumes

AddCommMonoidPartialOrderIsOrderedCancelAddMonoid