optionSubtype_symm_apply_apply_some

English

For x ∈ β and e : α ≃ { y : β // y ≠ x }, and a ∈ α, the image of some a under the inverse is some of the corresponding value.

Русский

Для x ∈ β и e : α ≃ { y : β // y ≠ x }, и a ∈ α, образ some a под обратным отображением равен some соответствующего значения.

LaTeX

$$$((\mathrm{optionSubtype} x).symm e : \mathrm{Option} \alpha \simeq \beta) (\mathrm{some} \, a) = \mathrm{some} (e a).$$$

Lean4

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

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