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
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip