optionSubtype_apply_apply — Mathlib

English

If x ∈ β and e is a witness of an equivalence with e none = x, then for any a ∈ α, optionSubtype x e a = ⟨e a, h⟩.

Русский

Если x ∈ β и e — свидетельство эквивалентности с e none = x, тогда для любого a ∈ α, optionSubtype x e a = ⟨e a, h⟩.

LaTeX

$$$\text{optionSubtype } x\ e\; a = \langle (e : \mathrm{Option} \alpha \simeq \beta) a, h \rangle.$$$

Lean4

@[simp]
theorem optionSubtype_apply_apply [DecidableEq β] (x : β) (e : { e : Option α ≃ β // e none = x }) (a : α) (h) :
    optionSubtype x e a = ⟨(e : Option α ≃ β) a, h⟩ :=
  rfl

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