Lines Matching defs:complete
7555 val complete = new_definition ("complete",
7556 ``complete s <=>
7608 ``!s:real->bool. compact s ==> complete s``,
7609 GEN_TAC THEN REWRITE_TAC[complete, compact] THEN
7624 ``complete univ(:real)``,
7625 REWRITE_TAC[complete, IN_UNIV] THEN X_GEN_TAC ``x:num->real`` THEN
7630 ASM_SIMP_TAC std_ss [BOUNDED_CLOSED_IMP_COMPACT, CLOSED_CLOSURE, complete] THEN
7637 ``!s:real->bool. complete s <=> closed s``,
7639 [REWRITE_TAC[complete, CLOSED_LIMPT, LIMPT_SEQUENTIAL] THEN
7645 REWRITE_TAC[complete, CLOSED_SEQUENTIAL_LIMITS] THEN DISCH_TAC THEN
7647 MP_TAC(REWRITE_RULE[complete] COMPLETE_UNIV) THEN
7655 REWRITE_TAC[REWRITE_RULE[complete, IN_UNIV] COMPLETE_UNIV]]);
8436 complete, COMPLETE_UNIV, IN_UNIV],
11356 REWRITE_TAC[complete] THEN MESON_TAC[CONVERGENT_IMP_CAUCHY]);
17081 complete s
17082 ==> complete(IMAGE f s)``,
17083 REPEAT GEN_TAC THEN SIMP_TAC std_ss [complete, EXISTS_IN_IMAGE] THEN
17382 ==> !s. complete s ==> complete(IMAGE f s)``,
17388 ==> (complete(IMAGE f s) <=> complete s)``,
18832 ``!f s c. complete s /\ ~(s = {}) /\
18871 UNDISCH_TAC ``complete s`` THEN DISCH_TAC THEN
18872 FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE [complete]) THEN