Lines Matching defs:convergent
119 val convergent = new_definition("convergent",
120 ���convergent f = ?l. f --> l���);
130 ���!f. convergent f = (f --> lim f)���,
131 GEN_TAC THEN REWRITE_TAC[convergent] THEN EQ_TAC THENL
261 ==> convergent f���,
274 REWRITE_TAC[convergent] THEN EXISTS_TAC ���sup(\x. ?n:num. x = f(n))��� THEN
317 ���!f. convergent f = convergent (\n. ~(f n))���,
318 GEN_TAC THEN REWRITE_TAC[convergent] THEN EQ_TAC THEN
330 ���!f. bounded(mr1, ^geq) f /\ mono f ==> convergent f���,
464 ���!f. cauchy f = convergent f���,
471 SUBGOAL_THEN ���convergent (\n. f(g(n):num))��� MP_TAC THENL
473 REWRITE_TAC[convergent] THEN DISCH_THEN(X_CHOOSE_TAC ���l:real���) THEN
502 REWRITE_TAC[convergent] THEN
534 (* We can displace a convergent series by 1 *)
1150 REWRITE_TAC[GSYM convergent] THEN
1639 RW_TAC std_ss [summable, sums, GSYM convergent]