Nuprl Lemma : vr_PEXT_implies_retract
vr_PEXT 
(
A:Type. (A (
f1:A 
A A. f2:A A A. x:A A. ((f1 (f2 x)) = x))))
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 :
CollapseTHEN: Error :CollapseTHEN,
CollapseTHENA: Error :CollapseTHENA,
Auto: Error :Auto,
exists: x:A. B[x],
product: x:A 
B[x],
all: x:A. B[x],
implies: P Q,
function: x:A B[x],
equal: s = t,
vr_PEXT: vr_PEXT,
prop: 
,
universe: Type,
member: t 
T,
uimplies: b supposing a,
sq_type: SQType(T),
uall: [x:A]. B[x],
isect: 
x:A. B[x],
subtype_rel: A 
r B,
tactic: Error :tactic,
lambda: 
x.A[x],
apply: f a,
limited-type: LimitedType
Lemmas :
subtype_base_sq,
vr_PEXT_implies_A_eq_AimpA,
vr_PEXT_wf
vr\_PEXT {}\mRightarrow{} (\mforall{}A:Type. (A {}\mRightarrow{} (\mexists{}f1:A {}\mrightarrow{} A {}\mrightarrow{} A. \mexists{}f2:A {}\mrightarrow{} A {}\mrightarrow{} A. \mforall{}x:A {}\mrightarrow{} A. ((f1 (f2 x)) = x))))
Date html generated:
2012_02_20-PM-03_34_04
Last ObjectModification:
2012_02_02-PM-01_55_29
Home
Index