optionCongr_one — Mathlib

English

For any type α, extending the identity permutation on α to the type Option α yields the identity permutation on Option α.

Русский

Для любого типа α отображение идентичности на α в расширение на тип Option α даёт тождественную перестановку на Option α.

LaTeX

$$$ (1 : \\mathrm{Perm}(\alpha)).\\mathrm{optionCongr} = 1 $$$

Lean4

@[simp]
theorem optionCongr_one {α : Type*} : (1 : Perm α).optionCongr = 1 :=
  Equiv.optionCongr_refl

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