Fri, 22 Mar 2013 10:41:43 +0100 move connected to HOL image; used to show intermediate value theorem
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51480
move connected to HOL image; used to show intermediate value theorem
Fri, 22 Mar 2013 10:41:43 +0100 move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51479
move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
Fri, 22 Mar 2013 10:41:43 +0100 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)
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51478
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)
Fri, 22 Mar 2013 10:41:43 +0100 clean up lemma_nest_unique and renamed to nested_sequence_unique
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51477
clean up lemma_nest_unique and renamed to nested_sequence_unique
Fri, 22 Mar 2013 10:41:43 +0100 simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51476
simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
Fri, 22 Mar 2013 10:41:43 +0100 introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51475
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
Fri, 22 Mar 2013 10:41:43 +0100 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51474
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
Fri, 22 Mar 2013 10:41:43 +0100 move first_countable_topology to the HOL image
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51473
move first_countable_topology to the HOL image
Fri, 22 Mar 2013 10:41:43 +0100 move metric_space to its own theory
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51472
move metric_space to its own theory
Fri, 22 Mar 2013 10:41:42 +0100 move topological_space to its own theory
hoelzl [Fri, 22 Mar 2013 10:41:42 +0100] rev 51471
move topological_space to its own theory
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip