optionSubtype_symm_apply_apply_coe

English

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

Русский

Для x ∈ β и e : α ≃ { y : β // y ≠ x }, и a ∈ α, приведённое значение равно e(a).

LaTeX

$$$\operatorname{Eq}\big( \operatorname{toFunLike}.coe \big( (\mathrm{optionSubtype} x).symm e \big).val \ a , e a \big).$$

Lean4

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

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