src/HOL/Library/Liminf_Limsup.thy
 changeset 61585 a9599d3d7610 parent 61245 b77bf45efe21 child 61730 2b775b888897
equal inserted replaced
61584:f06e5a5a4b46 61585:a9599d3d7610
`    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`