summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Regularity.thy

changeset 56212 | 3253aaf73a01 |

parent 56193 | c726ecfb22b6 |

child 56541 | 0e3abadbef39 |

1.1 --- a/src/HOL/Probability/Regularity.thy Tue Mar 18 21:02:33 2014 +0100 1.2 +++ b/src/HOL/Probability/Regularity.thy Tue Mar 18 22:11:46 2014 +0100 1.3 @@ -312,7 +312,7 @@ 1.4 case 2 1.5 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) 1.6 also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) - M K)" 1.7 - unfolding inner by (subst INFI_ereal_cminus) force+ 1.8 + unfolding inner by (subst INF_ereal_cminus) force+ 1.9 also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))" 1.10 by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed) 1.11 also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))" 1.12 @@ -331,7 +331,7 @@ 1.13 case 1 1.14 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) 1.15 also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) - M U)" 1.16 - unfolding outer by (subst SUPR_ereal_cminus) auto 1.17 + unfolding outer by (subst SUP_ereal_cminus) auto 1.18 also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))" 1.19 by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed) 1.20 also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"