Documentation

Mathlib.Data.Multiset.Antidiagonal

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.

source
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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Multiset.antidiagonal_coe {α : Type u_1} (l : List α) :
    Multiset.antidiagonal ↑l = ↑(List.revzip (Multiset.powersetAux l))
    source
    @[simp]
    theorem Multiset.antidiagonal_coe' {α : Type u_1} (l : List α) :
    Multiset.antidiagonal ↑l = ↑(List.revzip (Multiset.powersetAux' l))
    source
    @[simp]
    theorem Multiset.mem_antidiagonal {α : Type u_1} {s : Multiset α} {x : Multiset α × Multiset α} :
    x ∈ Multiset.antidiagonal s ↔ x.1 + x.2 = s

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

    source
    @[simp]
    theorem Multiset.antidiagonal_map_fst {α : Type u_1} (s : Multiset α) :
    Multiset.map Prod.fst (Multiset.antidiagonal s) = Multiset.powerset s
    source
    @[simp]
    theorem Multiset.antidiagonal_map_snd {α : Type u_1} (s : Multiset α) :
    Multiset.map Prod.snd (Multiset.antidiagonal s) = Multiset.powerset s
    source
    @[simp]
    theorem Multiset.antidiagonal_zero {α : Type u_1} :
    Multiset.antidiagonal 0 = {(0, 0)}
    source
    @[simp]
    theorem Multiset.antidiagonal_cons {α : Type u_1} (a : α) (s : Multiset α) :
    Multiset.antidiagonal (a ::ₘ s) = Multiset.map (Prod.map id (Multiset.cons a)) (Multiset.antidiagonal s) + Multiset.map (Prod.map (Multiset.cons a) id) (Multiset.antidiagonal s)
    source
    theorem Multiset.antidiagonal_eq_map_powerset {α : Type u_1} [DecidableEq α] (s : Multiset α) :
    Multiset.antidiagonal s = Multiset.map (fun (t : Multiset α) => (s - t, t)) (Multiset.powerset s)
    source
    @[simp]
    theorem Multiset.card_antidiagonal {α : Type u_1} (s : Multiset α) :
    Multiset.card (Multiset.antidiagonal s) = 2 ^ Multiset.card s
    source
    theorem Multiset.prod_map_add {α : Type u_1} {β : Type u_2} [CommSemiring β] {s : Multiset α} {f : α → β} {g : α → β} :
    Multiset.prod (Multiset.map (fun (a : α) => f a + g a) s) = Multiset.sum (Multiset.map (fun (p : Multiset α × Multiset α) => Multiset.prod (Multiset.map f p.1) * Multiset.prod (Multiset.map g p.2)) (Multiset.antidiagonal s))