option_symm_apply_none_iff — Mathlib

English

For any e : Option α ≃ Option β, e.symm none = none iff e none = none.

Русский

Для любой e: Option α ≃ Option β, e.symm none = none тогда и только тогда, когда e none = none.

LaTeX

$$$ e\text{-symm}\,\mathrm{none} = \mathrm{none} \iff e\,\mathrm{none} = \mathrm{none}. $$$

Lean4

@[simp]
theorem option_symm_apply_none_iff : e.symm none = none ↔ e none = none :=
  ⟨fun h => by simpa using (congr_arg e h).symm, fun h => by simpa using (congr_arg e.symm h).symm⟩

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