removeNone_symm — Mathlib

English

For any e : Option α ≃ Option β, the inverse of the induced equivalence removeNone e equals the induced equivalence on the inverse, i.e., (removeNone e).symm = removeNone e.symm.

Русский

Для любой e: Option α ≃ Option β обратное к полученной эквивалентности removeNone e равно эквивалентности, полученной из e.symm: (removeNone e).symm = removeNone e.symm.

LaTeX

$$$ (\mathrm{removeNone}\ e)^{\mathrm{symm}} = \mathrm{removeNone}\ e^{\mathrm{symm}}. $$$

Lean4

@[simp]
theorem removeNone_symm : (removeNone e).symm = removeNone e.symm :=
  rfl

Похожие утверждения