English
Let a be an element and s a multiset of a type α. The antidiagonal of the multiset a plus s is obtained by two parallel constructions: first, for every pair in the antidiagonal of s, add a to the second component; second, add a to the first component. The two resulting multisets are then added together.
Русский
Пусть a — элемент множества α, а s — мультимножество. Антидиагональ множества a + s получается двумя параллельными способами: к каждой паре из антидиагонали s прибавляем a ко второй компоненте; во второй копии прибавляем a к первой компоненте. Полученные мультимножества складываются.
LaTeX
$$$\\operatorname{antidiagonal}(a + s) = \\operatorname{map}(\\operatorname{Prod.map}(\mathrm{id},\\ \\operatorname{cons}(a)))\\bigl(\\operatorname{antidiagonal}(s)\\bigr) + \\operatorname{map}(\\operatorname{Prod.map}(\\operatorname{cons}(a),\\ \\mathrm{id}))\\bigl(\\operatorname{antidiagonal}(s)\\bigr).$$$
Lean4
@[simp]
theorem antidiagonal_cons (a : α) (s) :
antidiagonal (a ::ₘ s) =
map (Prod.map id (cons a)) (antidiagonal s) + map (Prod.map (cons a) id) (antidiagonal s) :=
Quotient.inductionOn s fun l ↦
by
simp only [revzip, reverse_append, quot_mk_to_coe, coe_eq_coe, powersetAux'_cons, cons_coe, map_coe,
antidiagonal_coe', coe_add]
rw [← zip_map, ← zip_map, zip_append, (_ : _ ++ _ = _)]
· congr
· simp only [List.map_id]
· rw [map_reverse]
· simp
· simp
