tuned proofs
authorhoelzl
Wed Mar 06 16:56:21 2013 +0100 (2013-03-06)
changeset 513648ee377823518
parent 51363 d4d00c804645
child 51365 6b5250100db8
tuned proofs
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 06 16:56:21 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 06 16:56:21 2013 +0100
     1.3 @@ -6315,20 +6315,18 @@
     1.4    show ?th unfolding homeomorphic_minimal
     1.5      apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
     1.6      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
     1.7 -    using assms apply (auto simp add: dist_commute)
     1.8 -    unfolding dist_norm
     1.9 -    apply (auto simp add: pos_divide_less_eq mult_strict_left_mono)
    1.10 -    unfolding continuous_on
    1.11 -    by (intro ballI tendsto_intros, simp)+
    1.12 +    using assms
    1.13 +    apply (auto intro!: continuous_on_intros
    1.14 +                simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
    1.15 +    done
    1.16  next
    1.17    show ?cth unfolding homeomorphic_minimal
    1.18      apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
    1.19      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
    1.20 -    using assms apply (auto simp add: dist_commute)
    1.21 -    unfolding dist_norm
    1.22 -    apply (auto simp add: pos_divide_le_eq)
    1.23 -    unfolding continuous_on
    1.24 -    by (intro ballI tendsto_intros, simp)+
    1.25 +    using assms
    1.26 +    apply (auto intro!: continuous_on_intros
    1.27 +                simp: dist_commute dist_norm pos_divide_le_eq mult_strict_left_mono)
    1.28 +    done
    1.29  qed
    1.30  
    1.31  text{* "Isometry" (up to constant bounds) of injective linear map etc.           *}