equal
deleted
inserted
replaced
915 |
915 |
916 lemma suminf_upper: |
916 lemma suminf_upper: |
917 fixes f :: "nat \<Rightarrow> ereal" |
917 fixes f :: "nat \<Rightarrow> ereal" |
918 assumes "\<And>n. 0 \<le> f n" |
918 assumes "\<And>n. 0 \<le> f n" |
919 shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)" |
919 shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)" |
920 unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def |
920 unfolding suminf_ereal_eq_SUPR[OF assms] |
921 by (auto intro: complete_lattice_class.Sup_upper) |
921 by (auto intro: complete_lattice_class.SUP_upper) |
922 |
922 |
923 lemma suminf_0_le: |
923 lemma suminf_0_le: |
924 fixes f :: "nat \<Rightarrow> ereal" |
924 fixes f :: "nat \<Rightarrow> ereal" |
925 assumes "\<And>n. 0 \<le> f n" |
925 assumes "\<And>n. 0 \<le> f n" |
926 shows "0 \<le> (\<Sum>n. f n)" |
926 shows "0 \<le> (\<Sum>n. f n)" |
1213 unfolding inf_min[symmetric] Liminf_at |
1213 unfolding inf_min[symmetric] Liminf_at |
1214 apply (subst inf_commute) |
1214 apply (subst inf_commute) |
1215 apply (subst SUP_inf) |
1215 apply (subst SUP_inf) |
1216 apply (intro SUP_cong[OF refl]) |
1216 apply (intro SUP_cong[OF refl]) |
1217 apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union) |
1217 apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union) |
1218 apply (simp add: INF_def del: inf_ereal_def) |
1218 apply (drule sym) |
1219 done |
1219 apply auto |
|
1220 by (metis INF_absorb centre_in_ball) |
1220 |
1221 |
1221 |
1222 |
1222 subsection {* monoset *} |
1223 subsection {* monoset *} |
1223 |
1224 |
1224 definition (in order) mono_set: |
1225 definition (in order) mono_set: |