Multiset.mem_antidiagonal
theorem Multiset.mem_antidiagonal :
∀ {α : Type u_1} {s : Multiset α} {x : Multiset α × Multiset α}, x ∈ s.antidiagonal ↔ x.1 + x.2 = s
The theorem `Multiset.mem_antidiagonal` can be described as follows:
For a given type `α`, a multiset `s` of that type, and a pair `x` which consists of two multisets of type `α`, the pair `x` is a member of the antidiagonal of `s` if and only if the sum of the elements of the pair `x` (denoted as `x.1 + x.2`) is equal to `s`. In other words, this theorem is about the condition under which a pair of multisets belongs to the antidiagonal of another multiset. The term 'antidiagonal' is used in the context of multisets to denote a collection of pairs of multisets that add up to a given multiset.
More concisely: For a multiset `s` of type `α`, a pair `(x, y)` of multisets of type `α` is in the antidiagonal of `s` if and only if `x + y = s`.
|
Multiset.antidiagonal_coe'
theorem Multiset.antidiagonal_coe' :
∀ {α : Type u_1} (l : List α), (↑l).antidiagonal = ↑(Multiset.powersetAux' l).revzip
The theorem `Multiset.antidiagonal_coe'` states that for any type `α` and any list `l` of type `α`, the antidiagonal of the multiset corresponding to `l` is equivalent to the list of reversed pairs of the powerset of `l`, where both are viewed as multisets. The antidiagonal of a multiset `s` includes all pairs `(t₁, t₂)` such that `t₁ + t₂ = s`, counted with multiplicities. This theorem links the antidiagonal of a multiset to operations on the list from which the multiset originated, specifically, generating the powerset and pairing each element with its corresponding element in the reverse list.
More concisely: The antidiagonal of a multiset formed from a list is equal to the multiset of reversed element pairs from the list's powerset.
|