decomposeOption_symm_of_none_apply

English

Applying the inverse of the decomposeOption equivalence to (none, e) yields i.map e for any i in Option α and e ∈ Perm α.

Русский

Применение обратного кодифицирования к паре (none, e) даёт i.map e для любого i ∈ Option α и e ∈ Perm α.

LaTeX

$$$ \\mathrm{decomposeOption}.\\mathrm{symm} (\\mathrm{none}, e)\\, i = i.\\mathrm{map}\\ e $$$

Lean4

theorem decomposeOption_symm_of_none_apply {α : Type*} [DecidableEq α] (e : Perm α) (i : Option α) :
    Equiv.Perm.decomposeOption.symm (none, e) i = i.map e := by simp

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