Step * of Lemma p-lift_wf

[A,B:Type]. ∀[P:A ⟶ ℙ]. ∀[d:x:A ⟶ Dec(P[x])]. ∀[f:{x:A| P[x]}  ⟶ B].  (p-lift(d;f) ∈ A ⟶ (B Top))
BY
(Unfold `p-lift` THEN Auto THEN (Fold `or` THEN Fold `decidable` 0⋅THEN Auto) }


Latex:


Latex:
\mforall{}[A,B:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:x:A  {}\mrightarrow{}  Dec(P[x])].  \mforall{}[f:\{x:A|  P[x]\}    {}\mrightarrow{}  B].
    (p-lift(d;f)  \mmember{}  A  {}\mrightarrow{}  (B  +  Top))


By


Latex:
(Unfold  `p-lift`  0  THEN  Auto  THEN  (Fold  `or`  0  THEN  Fold  `decidable`  0\mcdot{})  THEN  Auto)




Home Index