equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Liminf and Limsup on complete lattices *} |
5 header {* Liminf and Limsup on complete lattices *} |
6 |
6 |
7 theory Liminf_Limsup |
7 theory Liminf_Limsup |
8 imports "~~/src/HOL/Complex_Main" |
8 imports Complex_Main |
9 begin |
9 begin |
10 |
10 |
11 lemma le_Sup_iff_less: |
11 lemma le_Sup_iff_less: |
12 fixes x :: "'a :: {complete_linorder, inner_dense_linorder}" |
12 fixes x :: "'a :: {complete_linorder, inner_dense_linorder}" |
13 shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs") |
13 shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs") |