optionSubtype_symm_apply_symm_apply

English

For x ∈ β and e : α ≃ { y : β // y ≠ x }, and b ∈ { y : β // y ≠ x }, we have ((optionSubtype x).symm e).symm b = e.symm b.

Русский

Для x ∈ β, e : α ≃ { y : β // y ≠ x } и b ∈ { y : β // y ≠ x }, имеет место ((optionSubtype x).symm e).symm b = e.symm b.

LaTeX

$$$((\mathrm{optionSubtype} x).symm e).symm\ b = e.symm\ b.$$$

Lean4

@[simp]
theorem optionSubtype_symm_apply_symm_apply [DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x })
    (b : { y : β // y ≠ x }) : ((optionSubtype x).symm e : Option α ≃ β).symm b = e.symm b :=
  by
  simp only [optionSubtype, coe_fn_symm_mk, Subtype.coe_mk, Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]
  exact fun h => False.elim (b.property h)

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