summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

Fri, 22 Mar 2013 10:41:43 +0100
move connected to HOL image; used to show intermediate value theorem

move connected to HOL image; used to show intermediate value theorem

move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets

move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)

clean up lemma_nest_unique and renamed to nested_sequence_unique

simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano

introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it

generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun

move first_countable_topology to the HOL image

move metric_space to its own theory

move topological_space to its own theory