subtypeEquivRight_symm_apply — Mathlib

English

The inverse map of subtypeEquivRight e sends z : { x : α // q x } to ⟨ z.1, (e z.1).mpr z.2 ⟩.

Русский

Обратное отображение к subtypeEquivRight e отправляет z : { x : α // q x } в ⟨ z.1, (e z.1).mpr z.2 ⟩.

LaTeX

$$$( \\mathrm{subtypeEquivRight}\\ e)^{-1}\\ z = \\langle z.1, (e z.1).mpr z.2 \\rangle$$$

Lean4

theorem subtypeEquivRight_symm_apply {p q : α → Prop} (e : ∀ x, p x ↔ q x) (z : { x // q x }) :
    (subtypeEquivRight e).symm z = ⟨z, (e z.1).mpr z.2⟩ :=
  rfl

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