English
An equivalence e between sets s ⊆ α and t ⊆ α′ induces a linear equivalence between the finsupps supported on s and on t; i.e., there exists a canonical linear isomorphism between these two supported finsupp modules.
Русский
Эквивалентность e между множествами s ⊆ α и t ⊆ α′ порождает линейное эквивалентное отображение между функционалами с опорой в s и с опорой в t; то есть существует каноническое линейное изоморфизм между соответствующими модулями Finsupp.
LaTeX
$$$\\mathrm{congr}\\,s\\,t\\,e :\\; \\operatorname{supported} M R s \\;\\simeq_{R}\\; \\operatorname{supported} M R t$$$
Lean4
/-- An equivalence of sets induces a linear equivalence of `Finsupp`s supported on those sets. -/
noncomputable def congr {α' : Type*} (s : Set α) (t : Set α') (e : s ≃ t) : supported M R s ≃ₗ[R] supported M R t :=
by
haveI := Classical.decPred fun x => x ∈ s
haveI := Classical.decPred fun x => x ∈ t
exact Finsupp.supportedEquivFinsupp s ≪≫ₗ (Finsupp.domLCongr e ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm)
