equal
deleted
inserted
replaced
248 done |
248 done |
249 |
249 |
250 lemma homeomorphic_closed_intervals_real: |
250 lemma homeomorphic_closed_intervals_real: |
251 fixes a::real and b and c::real and d |
251 fixes a::real and b and c::real and d |
252 assumes "a<b" and "c<d" |
252 assumes "a<b" and "c<d" |
253 shows "{a..b} homeomorphic {c..d}" |
253 shows "{a..b} homeomorphic {c..d}" |
254 by (metis assms compact_interval continuous_on_id convex_real_interval(5) emptyE homeomorphic_convex_compact interior_atLeastAtMost_real mvt) |
254 using assms by (auto intro: homeomorphic_convex_compact) |
255 |
255 |
256 no_notation |
256 no_notation |
257 eucl_less (infix "<e" 50) |
257 eucl_less (infix "<e" 50) |
258 |
258 |
259 lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)" |
259 lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)" |