English
For a type α with decidable equality and a multiset s of α, the antidiagonal of s is obtained by taking every subset t of s (via the powerset) and pairing s − t with t.
Русский
Пусть α — тип с разрешённым равенством; для мультмножества s над α антидиагональ задаётся как образ множества подмножеств t ⊆ s под отображением t ↦ (s − t, t).
LaTeX
$$$s\\text{ antidiagonal} = s\\text{ powerset}.map(\\lambda t. (s - t, t)).$$$
Lean4
theorem antidiagonal_eq_map_powerset [DecidableEq α] (s : Multiset α) :
s.antidiagonal = s.powerset.map fun t ↦ (s - t, t) := by
induction s using Multiset.induction_on with
| empty => simp only [antidiagonal_zero, powerset_zero, Multiset.zero_sub, map_singleton]
| cons a s
hs =>
simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, Function.comp, Prod.map_apply, id, sub_cons,
erase_cons_head]
rw [add_comm]
congr 1
refine Multiset.map_congr rfl fun x hx ↦ ?_
rw [cons_sub_of_le _ (mem_powerset.mp hx)]
