# The antidiagonal on a multiset. #

The antidiagonal of a multiset s consists of all pairs (t₁, t₂) such that t₁ + t₂ = s. These pairs are counted with multiplicities.

def Multiset.antidiagonal {α : Type u_1} (s : ) :

The antidiagonal of a multiset s consists of all pairs (t₁, t₂) such that t₁ + t₂ = s. These pairs are counted with multiplicities.

Equations
Instances For
theorem Multiset.antidiagonal_coe {α : Type u_1} (l : List α) :
(l).antidiagonal = .revzip
@[simp]
theorem Multiset.antidiagonal_coe' {α : Type u_1} (l : List α) :
(l).antidiagonal = .revzip
@[simp]
theorem Multiset.mem_antidiagonal {α : Type u_1} {s : } {x : } :
x s.antidiagonal x.1 + x.2 = s

A pair (t₁, t₂) of multisets is contained in antidiagonal s if and only if t₁ + t₂ = s.

@[simp]
theorem Multiset.antidiagonal_map_fst {α : Type u_1} (s : ) :
Multiset.map Prod.fst s.antidiagonal = s.powerset
@[simp]
theorem Multiset.antidiagonal_map_snd {α : Type u_1} (s : ) :
Multiset.map Prod.snd s.antidiagonal = s.powerset
@[simp]
theorem Multiset.antidiagonal_zero {α : Type u_1} :
= {(0, 0)}
@[simp]
theorem Multiset.antidiagonal_cons {α : Type u_1} (a : α) (s : ) :
(a ::ₘ s).antidiagonal = Multiset.map (Prod.map id ()) s.antidiagonal + Multiset.map (Prod.map () id) s.antidiagonal
theorem Multiset.antidiagonal_eq_map_powerset {α : Type u_1} [] (s : ) :
s.antidiagonal = Multiset.map (fun (t : ) => (s - t, t)) s.powerset
@[simp]
theorem Multiset.card_antidiagonal {α : Type u_1} (s : ) :
Multiset.card s.antidiagonal = 2 ^ Multiset.card s