equal
deleted
inserted
replaced
98 qed |
98 qed |
99 |
99 |
100 lemma Liminf_eq: |
100 lemma Liminf_eq: |
101 assumes "eventually (\<lambda>x. f x = g x) F" |
101 assumes "eventually (\<lambda>x. f x = g x) F" |
102 shows "Liminf F f = Liminf F g" |
102 shows "Liminf F f = Liminf F g" |
103 by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto |
103 by (intro antisym Liminf_mono eventually_mono'[OF assms]) auto |
104 |
104 |
105 lemma Limsup_mono: |
105 lemma Limsup_mono: |
106 assumes ev: "eventually (\<lambda>x. f x \<le> g x) F" |
106 assumes ev: "eventually (\<lambda>x. f x \<le> g x) F" |
107 shows "Limsup F f \<le> Limsup F g" |
107 shows "Limsup F f \<le> Limsup F g" |
108 unfolding Limsup_def |
108 unfolding Limsup_def |
114 qed |
114 qed |
115 |
115 |
116 lemma Limsup_eq: |
116 lemma Limsup_eq: |
117 assumes "eventually (\<lambda>x. f x = g x) net" |
117 assumes "eventually (\<lambda>x. f x = g x) net" |
118 shows "Limsup net f = Limsup net g" |
118 shows "Limsup net f = Limsup net g" |
119 by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto |
119 by (intro antisym Limsup_mono eventually_mono'[OF assms]) auto |
120 |
120 |
121 lemma Liminf_le_Limsup: |
121 lemma Liminf_le_Limsup: |
122 assumes ntriv: "\<not> trivial_limit F" |
122 assumes ntriv: "\<not> trivial_limit F" |
123 shows "Liminf F f \<le> Limsup F f" |
123 shows "Liminf F f \<le> Limsup F f" |
124 unfolding Limsup_def Liminf_def |
124 unfolding Limsup_def Liminf_def |