English
Given f : α ≃ β, there is a canonical bijection between α →₀ M and β →₀ M obtained by transporting the domain along f.
Русский
С заданием f : α ≃ β существует каноническая биекция между α →₀ M и β →₀ M, получаемая переносом области определения вдоль f.
LaTeX
$$def equivMapDomain (f : α ≃ β) (l : α →₀ M) : β →₀ M$$
Lean4
/-- Given `f : α ≃ β`, we can map `l : α →₀ M` to `equivMapDomain f l : β →₀ M` (computably)
by mapping the support forwards and the function backwards. -/
def equivMapDomain (f : α ≃ β) (l : α →₀ M) : β →₀ M
where
support := l.support.map f.toEmbedding
toFun a := l (f.symm a)
mem_support_toFun a := by simp only [Finset.mem_map_equiv, mem_support_toFun]; rfl
