coe_optionSubtype_apply_apply — Mathlib

English

For x ∈ β and e : { e : Option α ≃ β // e none = x }, and b ∈ { y : β // y ≠ x }, the inverse image satisfies ↑((optionSubtype x).symm e) b = (e : Option α ≃ β) symm b.

Русский

Для x ∈ β и e : { e : Option α ≃ β // e none = x }, и b ∈ { y : β // y ≠ x }, обратное отображение удовлетворяет: ↑((optionSubtype x).symm e) b = e.symm b.

LaTeX

$$$\uparrow((\mathrm{optionSubtype}\ x\ e)^{-1} (b)) = e^{-1}(b).$$$

Lean4

@[simp]
theorem coe_optionSubtype_apply_apply [DecidableEq β] (x : β) (e : { e : Option α ≃ β // e none = x }) (a : α) :
    ↑(optionSubtype x e a) = (e : Option α ≃ β) a :=
  rfl

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