Lines Matching refs:mr1
63 ���$--> x x0 = (x tends x0)(mtop(mr1), ^geq)���,750);
204 ���!s. bounded(mr1, ^geq) s = ?k. !n. abs(s n) < k���,
222 ���!f k k'. (!n. k <= f(n) /\ f(n) <= k') ==> bounded(mr1, ^geq) f���,
247 ���!f. cauchy f ==> bounded(mr1, ^geq) f���,
261 ���!f. bounded(mr1, ^geq) f /\ (!m n:num. m >= n ==> f(m) >= f(n))
326 ���!f. bounded(mr1, ^geq)(\n. ~(f n)) = bounded(mr1, ^geq) f���,
331 ���!f. bounded(mr1, ^geq) f /\ mono f ==> convergent f���,
431 ���!s f. bounded(mr1,^geq) s ==> bounded(mr1,^geq) (\n. s(f n))���,
470 SUBGOAL_THEN ���bounded(mr1, ^geq)(\n. f(g(n):num))��� ASSUME_TAC THENL
676 DISCH_TAC THEN SUBGOAL_THEN ���bounded(mr1,^geq) f��� ASSUME_TAC THENL
687 SUBGOAL_THEN ���bounded(mr1, ^geq) g��� ASSUME_TAC THENL