Nuprl Definition : kripke2b-baire-seq

kripke2b-baire-seq(a;x;F) ==
  λb.if eq-finite-seqs(a;cantor2baire(b);x)
     then min-inc-seq(cantor2baire(b);fst((F cantor2baire(b)));(a x) + 1)
     else 0
     fi 


Definitions occuring in Statement :  cantor2baire: cantor2baire(a),  eq-finite-seqs: eq-finite-seqs(a;b;x),  min-inc-seq: min-inc-seq(a;n;k),  ifthenelse: if b then t else f fi ,  pi1: fst(t),  apply: f a,  lambda: λx.A[x],  add: n + m,  natural_number: $n
Definitions occuring in definition :  natural_number: $n,  apply: f a,  add: n + m,  cantor2baire: cantor2baire(a),  pi1: fst(t),  min-inc-seq: min-inc-seq(a;n;k),  eq-finite-seqs: eq-finite-seqs(a;b;x),  ifthenelse: if b then t else f fi ,  lambda: λx.A[x]
FDL editor aliases :  kripke2b-baire-seq
Latex:
kripke2b-baire-seq(a;x;F)  ==
    \mlambda{}b.if  eq-finite-seqs(a;cantor2baire(b);x)
          then  min-inc-seq(cantor2baire(b);fst((F  cantor2baire(b)));(a  x)  +  1)
          else  0
          fi 


Date html generated: 2017_04_21-AM-11_22_48
Last ObjectModification: 2017_04_20-PM-04_21_13

Theory : continuity


Home Index