English
Let e be a bijection between index types α1 and α2, and let v be a finitely supported M-valued function on α1. Then applying the domain-congruence induced by e to v yields the same result as applying the standard domain-congruence to v:
Русский
Пусть e — биекция между индексами α1 и α2, и пусть v — линейно ограниченная по поддержке функция с значениями в M на α1. Тогда применение согласования домена, индукции по e к v, совпадает с обычным согласованием домена по e к v.
LaTeX
$$$(\mathrm{domLCongr}\,e : (\alpha_1 \to_0 M) \simeq_\sigma (\alpha_2 \to_0 M))\,v = \mathrm{domCongr}\,e\,v$$$
Lean4
@[simp]
theorem domLCongr_apply {α₁ : Type*} {α₂ : Type*} (e : α₁ ≃ α₂) (v : α₁ →₀ M) :
(Finsupp.domLCongr e : _ ≃ₗ[R] _) v = Finsupp.domCongr e v :=
rfl
