English
For any equivalence e: α ≃ β, there is an induced equivalence between Option α and Option β given by mapping Some a to Some (e a) and None to None.
Русский
Для любого эквивалентности e: α ≃ β существует эквивалентность между Option α и Option β, отправляющая Some a ↦ Some (e a) и None ↦ None.
LaTeX
$$$\\text{Option }\\alpha \\simeq \\text{Option }\\beta$ with $\\text{toFun}=\\text{Option.map } e$ and $\\text{invFun}=\\text{Option.map } e^{-1}$.$$
Lean4
/-- A universe-polymorphic version of `EquivFunctor.mapEquiv Option e`. -/
@[simps (attr := grind =) apply]
def optionCongr (e : α ≃ β) : Option α ≃ Option β
where
toFun := Option.map e
invFun := Option.map e.symm
left_inv x := (Option.map_map _ _ _).trans <| e.symm_comp_self.symm ▸ congr_fun Option.map_id x
right_inv x := (Option.map_map _ _ _).trans <| e.self_comp_symm.symm ▸ congr_fun Option.map_id x
