Nuprl Lemma : vr_PEXT_implies_fixpoint
vr_PEXT 
(
A:Type. (A (
F:A 
A A. f:A A. ((F f) = (f (F f))))))
Proof not projected
Definitions occuring in Statement :
vr_PEXT: vr_PEXT,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x],
universe: Type,
equal: s = t
Definitions :
D: Error :D,
lambda: 
x.A[x],
apply: f a,
CollapseTHENA: Error :CollapseTHENA,
CollapseTHEN: Error :CollapseTHEN,
Auto: Error :Auto,
exists: x:A. B[x],
product: x:A 
B[x],
function: x:A B[x],
universe: Type,
vr_PEXT: vr_PEXT,
implies: P Q,
all: x:A. B[x],
equal: s = t,
member: t 
T,
prop: 
,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
limited-type: LimitedType,
uimplies: b supposing a,
sq_type: SQType(T),
subtype_rel: A 
r B
Lemmas :
subtype_base_sq,
vr_PEXT_implies_retract,
vr_PEXT_wf
vr\_PEXT {}\mRightarrow{} (\mforall{}A:Type. (A {}\mRightarrow{} (\mexists{}F:A {}\mrightarrow{} A {}\mrightarrow{} A. \mforall{}f:A {}\mrightarrow{} A. ((F f) = (f (F f))))))
Date html generated:
2012_02_20-PM-03_34_08
Last ObjectModification:
2012_02_02-PM-01_55_30
Home
Index