English
An equivalence between Option types induces an equivalence between their underlying types by collapsing None in a canonical way.
Русский
Эквивалентность между типами Option приводит к эквивалентности между базовыми типами путём канонического устранения значения None.
LaTeX
$$$\\text{removeNone}: (\\text{Option }\\alpha) \\simeq (\\text{Option }\\beta) \\to \\alpha \\simeq \\beta$$$
Lean4
/-- Given an equivalence between two `Option` types, eliminate `none` from that equivalence by
mapping `e.symm none` to `e none`. -/
def removeNone : α ≃ β where
toFun := removeNone_aux e
invFun := removeNone_aux e.symm
left_inv := removeNone_aux_inv e
right_inv := removeNone_aux_inv e.symm
