| Fri, 22 Mar 2013 10:41:43 +0100 | hoelzl | move continuous_on_inv to HOL image (simplifies isCont_inverse_function) | changeset | files |
| Fri, 22 Mar 2013 10:41:43 +0100 | hoelzl | move connected to HOL image; used to show intermediate value theorem | changeset | files |
| Fri, 22 Mar 2013 10:41:43 +0100 | hoelzl | move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets | changeset | files |