English
If f is an equivalence M ≃ N with f(0) = 0 and f.symm(0) = 0, then mapRange f hf hf' induces an equivalence between α →₀ M and α →₀ N, with inverse mapRange f.symm hf' hf.
Русский
Пусть f: M ≃ N удовлетворяет f(0)=0 и f.symm(0)=0. Тогда отображение mapRange f hf hf' устанавливает эквиваленцию между α →₀ M и α →₀ N, где обратное отображение — mapRange f.symm hf' hf.
LaTeX
$$$mapRange\\ f\\ hf\\ hf' : (\\alpha \\to_0 M) \\simeq (\\alpha \\to_0 N)$$$
Lean4
/-- `Finsupp.mapRange` as an equiv. -/
@[simps apply]
def equiv (f : M ≃ N) (hf : f 0 = 0) (hf' : f.symm 0 = 0) : (α →₀ M) ≃ (α →₀ N)
where
toFun := (mapRange f hf : (α →₀ M) → α →₀ N)
invFun := (mapRange f.symm hf' : (α →₀ N) → α →₀ M)
left_inv
x := by
rw [← mapRange_comp] <;> simp_rw [Equiv.symm_comp_self]
· exact mapRange_id _
· rfl
right_inv
x := by
rw [← mapRange_comp] <;> simp_rw [Equiv.self_comp_symm]
· exact mapRange_id _
· rfl
