optionCongr_injective — Mathlib

English

Equivalences between Option α and β that send none to x are equivalent to equivalences between α and {y ∈ β | y ≠ x}.

Русский

Эквивалентости между Option α и β, отправляющие none в x, эквивалентны эквивалентостям между α и {y ∈ β | y ≠ x}.

LaTeX

$$$\{e : \mathrm{Option} \alpha \simeq \beta \,|\, e(\mathrm{none}) = x\} \simeq (\alpha \simeq \{ y : \beta \;\vert\; y \neq x \}).$$$

Lean4

theorem optionCongr_injective : Function.Injective (optionCongr : α ≃ β → Option α ≃ Option β) :=
  Function.LeftInverse.injective removeNone_optionCongr

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