English
Given a bijection f : α ≃ β, there is a canonical equivalence (Equiv) between Finsupp α M and Finsupp β M, called equivCongrLeft.
Русский
С заданной биекцией f: α ≃ β существует каноническое эквивалентное отображение между α →₀ M и β →₀ M, обозначаемое как equivCongrLeft.
LaTeX
$$def equivCongrLeft (f : α ≃ β) : (α →₀ M) ≃ (β →₀ M)$$
Lean4
/-- Given `f : α ≃ β`, the finitely supported function spaces are also in bijection:
`(α →₀ M) ≃ (β →₀ M)`.
This is the finitely-supported version of `Equiv.piCongrLeft`. -/
def equivCongrLeft (f : α ≃ β) : (α →₀ M) ≃ (β →₀ M) := by
refine ⟨equivMapDomain f, equivMapDomain f.symm, fun f => ?_, fun f => ?_⟩ <;> ext x <;>
simp only [equivMapDomain_apply, Equiv.symm_symm, Equiv.symm_apply_apply, Equiv.apply_symm_apply]
