English
Let e be an additive equivalence between μ and μ'. Then applying the addEquiv e to finsuppAntidiag s n yields a subset of finsuppAntidiag s (e n). In other words, the antidiagonal structure is preserved up to the additive equivalence.
Русский
Пусть e — добавочное эквивалентность между μ и μ'. Тогда отображение finsuppAntidiag s n через addEquiv e содержит подмножество finsuppAntidiag s (e n). Антидиагональная структура сохраняется по отношению к эквивалентности сложения.
LaTeX
$$$(finsuppAntidiag\ s\ n).map( mapRange.addEquiv\ e).toEmbedding \subseteq\ finsuppAntidiag\ s\ (e\ n)$$$
Lean4
theorem mapRange_finsuppAntidiag_subset {e : μ ≃+ μ'} {s : Finset ι} {n : μ} :
(finsuppAntidiag s n).map (mapRange.addEquiv e).toEmbedding ⊆ finsuppAntidiag s (e n) :=
by
intro f
simp only [mem_map, mem_finsuppAntidiag']
rintro ⟨g, ⟨hsum, hsupp⟩, rfl⟩
simp only [AddEquiv.toEquiv_eq_coe, mapRange.addEquiv_toEquiv, Equiv.coe_toEmbedding, mapRange.equiv_apply,
EquivLike.coe_coe]
constructor
· rw [sum_mapRange_index (fun _ ↦ rfl), ← hsum, _root_.map_finsuppSum]
· exact subset_trans (support_mapRange) hsupp
