English
For any additive equivalence e, the image of finsuppAntidiag s n under mapRange.addEquiv e equals finsuppAntidiag s (e n).
Русский
Для любой добавочной эквивалентности e образ finsuppAntidiag s n через mapRange.addEquiv e равен finsuppAntidiag s (e n).
LaTeX
$$$(finsuppAntidiag\ s\ n).map( mapRange.addEquiv\ e).toEmbedding = finsuppAntidiag\ s\ (e\ n)$$$
Lean4
theorem mapRange_finsuppAntidiag_eq {e : μ ≃+ μ'} {s : Finset ι} {n : μ} :
(finsuppAntidiag s n).map (mapRange.addEquiv e).toEmbedding = finsuppAntidiag s (e n) :=
by
ext f
constructor
· apply mapRange_finsuppAntidiag_subset
· set h := (mapRange.addEquiv e).toEquiv with hh
intro hf
have : n = e.symm (e n) := (AddEquiv.eq_symm_apply e).mpr rfl
rw [mem_map_equiv, this]
apply mapRange_finsuppAntidiag_subset
rw [← mem_map_equiv]
convert hf
rw [map_map, hh]
convert map_refl
apply Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding
