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 : Multiset α) : Multiset (Multiset α × Multiset α)

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

Equations

• s.antidiagonal = Quot.liftOn s (fun (l : List α) => ↑(Multiset.powersetAux l).revzip) ⋯

theorem Multiset.antidiagonal_coe {α : Type u_1} (l : List α) : (↑l).antidiagonal = ↑(Multiset.powersetAux l).revzip

@[simp]

theorem Multiset.antidiagonal_coe' {α : Type u_1} (l : List α) : (↑l).antidiagonal = ↑(Multiset.powersetAux' l).revzip

@[simp]

theorem Multiset.mem_antidiagonal {α : Type u_1} {s : Multiset α} {x : Multiset α × Multiset α} : 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 α) : Multiset.map Prod.fst s.antidiagonal = s.powerset

@[simp]

theorem Multiset.antidiagonal_map_snd {α : Type u_1} (s : Multiset α) : Multiset.map Prod.snd s.antidiagonal = s.powerset

@[simp]

theorem Multiset.antidiagonal_zero {α : Type u_1} : Multiset.antidiagonal 0 = {(0, 0)}

@[simp]

theorem Multiset.antidiagonal_cons {α : Type u_1} (a : α) (s : Multiset α) : (a ::ₘ s).antidiagonal = Multiset.map (Prod.map id (Multiset.cons a)) s.antidiagonal + Multiset.map (Prod.map (Multiset.cons a) id) s.antidiagonal

theorem Multiset.antidiagonal_eq_map_powerset {α : Type u_1} [DecidableEq α] (s : Multiset α) : s.antidiagonal = Multiset.map (fun (t : Multiset α) => (s - t, t)) s.powerset

@[simp]

theorem Multiset.card_antidiagonal {α : Type u_1} (s : Multiset α) : s.antidiagonal.card = 2 ^ s.card