subtypeOrEquiv_symm_inl — Mathlib

English

The inverse of subtypeOrEquiv on inl x is ⟨x, p x⟩ with left component.

Русский

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

LaTeX

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

Lean4

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

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