Nuprl Definition : real-cont-ps

real-cont-ps(k;a;b;f;x;N) ==
uniform-continuity-pi-search(
λm@0.(primrec(x;λ%4,m,%5. ⋅;λi,x,%7,m,%8. case FiniteCantorDecide(λs.if f

                                                                  cantor-to-interval(a;b;λx.if (x) < ((i + 1) - 1)

                                                                                               then s x

                                                                                               else tt)

                                                                  (N * k)=f

                                                                          cantor-to-interval(a;b;λx.if (x) < ((i + 1)

                                                                                                      - 1)

                                                                                                       then s x

                                                                                                       else ff)

                                                                          (N * k)

                                                               then inr (λ_.⋅)

                                                               else (inl (λ_.⋅));(i + 1) - 1;λx.x)

                                    of inl(x1) =>
                                    let x1,f = x1
                                    in inr (λ%14.⋅)
                                    | inr(x1) =>

                                    if m=(i + 1) - 1 then inl (λf,g,%3. ⋅) else (x (λf,g,%3. ⋅) m ⋅))

        (λf,g,eq. ⋅)
        m@0
        ⋅);
  x;0)

Definitions occuring in Statement : cantor-to-interval: cantor-to-interval(a;b;f), uniform-continuity-pi-search: uniform-continuity-pi-search, simple-finite-cantor-decider: FiniteCantorDecide(dcdr;n;F), primrec: primrec(n;b;c), bfalse: ff, btrue: tt, it: ⋅, less: if (a) < (b) then c else d, int_eq: if a=b then c else d, apply: f a, lambda: λx.A[x], spread: spread def, decide: case b of inl(x) => s[x] | inr(y) => t[y], inr: inr x , inl: inl x, multiply: n * m, subtract: n - m, add: n + m, natural_number: $n
Definitions occuring in definition : uniform-continuity-pi-search: uniform-continuity-pi-search, primrec: primrec(n;b;c), decide: case b of inl(x) => s[x] | inr(y) => t[y], simple-finite-cantor-decider: FiniteCantorDecide(dcdr;n;F), btrue: tt, cantor-to-interval: cantor-to-interval(a;b;f), less: if (a) < (b) then c else d, bfalse: ff, multiply: n * m, spread: spread def, inr: inr x , int_eq: if a=b then c else d, subtract: n - m, add: n + m, inl: inl x, apply: f a, lambda: λx.A[x], it: ⋅, natural_number: $n
FDL editor aliases : real-cont-ps

Latex:
real-cont-ps(k;a;b;f;x;N) == uniform-continuity-pi-search( \mlambda{}m@0.(primrec(x;\mlambda{}\%4,m,\%5. \mcdot{}; \mlambda{}i,x,\%7,m,\%8. case FiniteCantorDecide(\mlambda{}s.if f cantor-to-interval(a;b;\mlambda{}x.if (x) < ((i + 1) - 1) then s x else tt) (N * k)=f cantor-to-interval(a;b;\mlambda{}x....) (N * k) then inr (\mlambda{}$_{}$.\mcdot{}) else (inl (\mlambda{}$_{}$.\mcdot{}));(i\000C + 1) - 1;\mlambda{}x.x) of inl(x1) => let x1,f = x1 in inr (\mlambda{}\%14.\mcdot{}) | inr(x1) => if m=(i + 1) - 1 then inl (\mlambda{}f,g,\%3. \mcdot{}) else (x (\mlambda{}f,g,\%3. \mcdot{}) m \mcdot{})) (\mlambda{}f,g,eq. \mcdot{}) m@0 \mcdot{}); x;0) Date html generated: 2018_05_22-PM-02_10_41 Last ObjectModification: 2018_01_15-PM-03_22_17 Theory : reals Home Index