Thu, 17 Jan 2013 15:17:48 +0100 | wenzelm | tuned proofs; | changeset | files |
Thu, 17 Jan 2013 14:38:12 +0100 | hoelzl | simplified prove of compact_imp_bounded | changeset | files |
Thu, 17 Jan 2013 13:58:02 +0100 | hoelzl | use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma | changeset | files |
Thu, 17 Jan 2013 13:21:34 +0100 | hoelzl | move auxiliary lemma to top | changeset | files |