Nuprl Lemma : lift_ctr_wf
[a4,F:Type]. [f:F  a4].  (lift_ctr(f)    F  (  a4))
Proof
Definitions occuring in Statement : 
lift_ctr: lift_ctr(f), 
uall: [x:A]. B[x], 
member: t  T, 
function: x:A  B[x], 
product: x:A  B[x], 
int: , 
universe: Type
Definitions : 
uall: [x:A]. B[x], 
member: t  T, 
lift_ctr: lift_ctr(f)
\mforall{}[a4,F:Type].  \mforall{}[f:F  {}\mrightarrow{}  a4].    (lift\_ctr(f)  \mmember{}  \mBbbZ{}  \mtimes{}  F  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  a4))
Date html generated:
2013_03_20-AM-09_45_35
Last ObjectModification:
2013_02_15-PM-06_01_18
Home
Index