equal
deleted
inserted
replaced
27 apply (rule INF_lower2[where i=1]) |
27 apply (rule INF_lower2[where i=1]) |
28 apply simp_all |
28 apply simp_all |
29 done |
29 done |
30 |
30 |
31 text \<open> |
31 text \<open> |
32 The name @{text continuous} is already taken in @{text "Complex_Main"}, so we use |
32 The name \<open>continuous\<close> is already taken in \<open>Complex_Main\<close>, so we use |
33 @{text "sup_continuous"} and @{text "inf_continuous"}. These names appear sometimes in literature |
33 \<open>sup_continuous\<close> and \<open>inf_continuous\<close>. These names appear sometimes in literature |
34 and have the advantage that these names are duals. |
34 and have the advantage that these names are duals. |
35 \<close> |
35 \<close> |
36 |
36 |
37 named_theorems order_continuous_intros |
37 named_theorems order_continuous_intros |
38 |
38 |