subtypeOrEquiv_symm_inr — Mathlib

English

The inverse of subtypeOrEquiv on inr x is ⟨x, q x⟩ with right component.

Русский

Обратный к subtypeOrEquiv на inr x равен ⟨x, q x⟩ с правой составляющей.

LaTeX

$$$(subtypeOrEquiv p q h)^{-1}(\\mathrm{inr} x) = \\langle x, \\text{Or.inr } x.prop \\rangle$$$

Lean4

@[simp, grind =]
theorem subtypeOrEquiv_symm_inr (p q : α → Prop) [DecidablePred p] (h : Disjoint p q) (x : { x // q x }) :
    (subtypeOrEquiv p q h).symm (Sum.inr x) = ⟨x, Or.inr x.prop⟩ :=
  rfl

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