src/HOL/Library/Order_Continuity.thy
changeset 69313 b021008c5397
parent 63979 95c3ae4baba8
child 69661 a03a63b81f44
     1.1 --- a/src/HOL/Library/Order_Continuity.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Library/Order_Continuity.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -76,7 +76,7 @@
     1.4    assume M: "mono M"
     1.5    then have "mono (\<lambda>i. g (M i))"
     1.6      using sup_continuous_mono[OF g] by (auto simp: mono_def)
     1.7 -  with M show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
     1.8 +  with M show "f (g (Sup (M ` UNIV))) = (SUP i. f (g (M i)))"
     1.9      by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
    1.10  qed
    1.11  
    1.12 @@ -274,7 +274,7 @@
    1.13    assume M: "antimono M"
    1.14    then have "antimono (\<lambda>i. g (M i))"
    1.15      using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
    1.16 -  with M show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
    1.17 +  with M show "f (g (Inf (M ` UNIV))) = (INF i. f (g (M i)))"
    1.18      by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
    1.19  qed
    1.20