Tue, 09 Jun 2009 10:23:41 -0700 | huffman | instance heine_borel < complete_space; generalize many lemmas to class heine_borel | changeset | files |
Tue, 09 Jun 2009 09:38:56 -0700 | huffman | new class heine_borel for lemma bounded_closed_imp_compact; instances for real, ^ | changeset | files |
Mon, 08 Jun 2009 19:45:24 -0700 | huffman | generalize compact/closure lemmas | changeset | files |
Mon, 08 Jun 2009 19:18:47 -0700 | huffman | add lemma complete_imp_closed | changeset | files |
Mon, 08 Jun 2009 17:15:22 -0700 | huffman | generalize constant 'bounded' to class metric_space | changeset | files |
Mon, 08 Jun 2009 15:46:14 -0700 | huffman | generalize lemmas compact_imp_bounded, compact_imp_closed | changeset | files |
Mon, 08 Jun 2009 15:00:37 -0700 | huffman | generalize more lemmas | changeset | files |