equivOption — Mathlib

English

There is a (classical) equivalence between Part α and Option α, given by toOption and its inverse ofOption.

Русский

Существует классическая эквивалентность между Part α и Option α, задаваемая отображениями toOption и его обратной toOption.

LaTeX

$$$ \mathrm{Part}(\alpha) \simeq \mathrm{Option}(\alpha) $$$

Lean4

/-- `Part α` is (classically) equivalent to `Option α`. -/
noncomputable def equivOption : Part α ≃ Option α :=
  haveI := Classical.dec
  ⟨fun o => toOption o, ofOption, fun o => of_toOption o, fun o => Eq.trans (by dsimp; congr) (to_ofOption o)⟩

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