optionSubtype_apply_symm_apply — Mathlib

English

For x ∈ β and e : α ≃ { y : β // y ≠ x }, and a ∈ α, the coerced inverse applied to a equals e(a).

Русский

Для x ∈ β и e : α ≃ { y : β // y ≠ x }, и a ∈ α, сопряжённое обратное, применённое к a, равно e(a).

LaTeX

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

Lean4

@[simp]
theorem optionSubtype_apply_symm_apply [DecidableEq β] (x : β) (e : { e : Option α ≃ β // e none = x })
    (b : { y : β // y ≠ x }) : ↑((optionSubtype x e).symm b) = (e : Option α ≃ β).symm b :=
  by
  dsimp only [optionSubtype]
  simp

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