equal
deleted
inserted
replaced
28 lemma INF_pair: |
28 lemma INF_pair: |
29 fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice" |
29 fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice" |
30 shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))" |
30 shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))" |
31 by (rule antisym) (auto intro!: INF_greatest INF_lower2) |
31 by (rule antisym) (auto intro!: INF_greatest INF_lower2) |
32 |
32 |
33 subsubsection \<open>@{text Liminf} and @{text Limsup}\<close> |
33 subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close> |
34 |
34 |
35 definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where |
35 definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where |
36 "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)" |
36 "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)" |
37 |
37 |
38 definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where |
38 definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where |