English
An equivalence e: α ≃ β induces an equivalence between lists: List α ≃ List β, with toFun given by List.map e and invFun by List.map e.symm.
Русский
Эквивалентность e: α ≃ β порождает эквивалентность между списками: List α ≃ List β, где отображение toFun есть List.map e, а обратное List.map e.symm.
LaTeX
$$$ \\text{listEquivOfEquiv }(e) : \\text{List } \\alpha \\simeq \\text{List } \\beta,\\; \\text{toFun} = \\text{List.map } e,\\; \\text{invFun} = \\text{List.map } e^{-1}$$$
Lean4
/-- An equivalence between `α` and `β` generates an equivalence between `List α` and `List β`. -/
def listEquivOfEquiv {α β} (e : α ≃ β) : List α ≃ List β
where
toFun := List.map e
invFun := List.map e.symm
left_inv l := by rw [List.map_map, e.symm_comp_self, List.map_id]
right_inv l := by rw [List.map_map, e.self_comp_symm, List.map_id]
