Nuprl Definition : vr_AC1
vr_AC1 ==
[T:Type]
F:T 
'. ((X:T . ((F X) 
(
x:T. (X x)))) (f:T T. X:T . ((F X) (X (f X)))))
Definitions occuring in Statement :
uall: [x:A]. B[x],
prop: ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x],
universe: Type
FDL editor aliases :
vr_AC1
vr\_AC1 ==
\mforall{}[T:Type]
\mforall{}F:T {}\mrightarrow{} \mBbbP{} {}\mrightarrow{} \mBbbU{}'
((\mforall{}X:T {}\mrightarrow{} \mBbbP{}. ((F X) {}\mRightarrow{} (\mexists{}x:T. (X x)))) {}\mRightarrow{} (\mexists{}f:T {}\mrightarrow{} \mBbbP{} {}\mrightarrow{} T. \mforall{}X:T {}\mrightarrow{} \mBbbP{}. ((F X) {}\mRightarrow{} (X (f X)))))
Date html generated:
2012_02_20-PM-03_33_22
Last ObjectModification:
2012_02_02-PM-01_55_19
Home
Index