src/HOL/Library/Order_Continuity.thy
changeset 63540 f8652d0534fa
parent 62374 cb27a55d868a
child 63979 95c3ae4baba8
     1.1 --- a/src/HOL/Library/Order_Continuity.thy	Fri Jul 22 08:02:37 2016 +0200
     1.2 +++ b/src/HOL/Library/Order_Continuity.thy	Fri Jul 22 11:00:43 2016 +0200
     1.3 @@ -72,10 +72,11 @@
     1.4    shows "sup_continuous (\<lambda>x. f (g x))"
     1.5    unfolding sup_continuous_def
     1.6  proof safe
     1.7 -  fix M :: "nat \<Rightarrow> 'c" assume "mono M"
     1.8 -  moreover then have "mono (\<lambda>i. g (M i))"
     1.9 +  fix M :: "nat \<Rightarrow> 'c"
    1.10 +  assume M: "mono M"
    1.11 +  then have "mono (\<lambda>i. g (M i))"
    1.12      using sup_continuous_mono[OF g] by (auto simp: mono_def)
    1.13 -  ultimately show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
    1.14 +  with M show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
    1.15      by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
    1.16  qed
    1.17  
    1.18 @@ -269,10 +270,11 @@
    1.19    shows "inf_continuous (\<lambda>x. f (g x))"
    1.20    unfolding inf_continuous_def
    1.21  proof safe
    1.22 -  fix M :: "nat \<Rightarrow> 'c" assume "antimono M"
    1.23 -  moreover then have "antimono (\<lambda>i. g (M i))"
    1.24 +  fix M :: "nat \<Rightarrow> 'c"
    1.25 +  assume M: "antimono M"
    1.26 +  then have "antimono (\<lambda>i. g (M i))"
    1.27      using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
    1.28 -  ultimately show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
    1.29 +  with M show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
    1.30      by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
    1.31  qed
    1.32