equal
deleted
inserted
replaced
616 "!!(X::nat=>real). [| ALL m n. m <= n --> X m <= X n; \ |
616 "!!(X::nat=>real). [| ALL m n. m <= n --> X m <= X n; \ |
617 \ isLub (UNIV::real set) {x. EX n. X n = x} (X ma) \ |
617 \ isLub (UNIV::real set) {x. EX n. X n = x} (X ma) \ |
618 \ |] ==> ALL n. ma <= n --> X n = X ma"; |
618 \ |] ==> ALL n. ma <= n --> X n = X ma"; |
619 by (Step_tac 1); |
619 by (Step_tac 1); |
620 by (dres_inst_tac [("y","X n")] isLubD2 1); |
620 by (dres_inst_tac [("y","X n")] isLubD2 1); |
621 by (ALLGOALS(blast_tac (claset() addDs [real_le_anti_sym]))); |
621 by (ALLGOALS(blast_tac (claset() addDs [order_antisym]))); |
622 qed "lemma_converg1"; |
622 qed "lemma_converg1"; |
623 |
623 |
624 (*------------------------------------------------------------------- |
624 (*------------------------------------------------------------------- |
625 The best of both world: Easier to prove this result as a standard |
625 The best of both world: Easier to prove this result as a standard |
626 theorem and then use equivalence to "transfer" it into the |
626 theorem and then use equivalence to "transfer" it into the |