Nuprl Definition : bar_26_3a
bar_26_3a{i:l}(R) == (
a:
List. Dec(R a)) 
bar_fwd_fim(R) (A: List 
. bar_bwd_fim(R;A))
Definitions occuring in Statement :
bar_bwd_fim: bar_bwd_fim(R;A),
bar_fwd_fim: bar_fwd_fim(R),
nat: ,
decidable: Dec(P),
prop: ,
all: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x]
FDL editor aliases :
bar_26_3a
bar\_26\_3a\{i:l\}(R) == (\mforall{}a:\mBbbN{} List. Dec(R a)) {}\mRightarrow{} bar\_fwd\_fim(R) {}\mRightarrow{} (\mforall{}A:\mBbbN{} List {}\mrightarrow{} \mBbbP{}. bar\_bwd\_fim(R;A))
Date html generated:
2013_03_20-AM-10_31_56
Last ObjectModification:
2013_02_28-PM-07_26_34
Home
Index