optionSubtype_symm_apply_apply_none

English

For any x ∈ β and e : α ≃ { y : β // y ≠ x }, the inverse applied to none yields x.

Русский

Для любого x ∈ β и e : α ≃ { y : β // y ≠ x }, применение обратного к none даёт x.

LaTeX

$$$((\mathrm{optionSubtype} x).symm e : \mathrm{Option} \alpha \simeq \beta) \; \mathrm{none} = x.$$$

Lean4

@[simp]
theorem optionSubtype_symm_apply_apply_none [DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x }) :
    ((optionSubtype x).symm e : Option α ≃ β) none = x :=
  rfl

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