Nuprl Lemma : lift_ctr

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