summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Probability/Borel_Space.thy

changeset 44928 | 7ef6505bde7f |

parent 44890 | 22f665a2e91c |

child 45287 | 97df8c08291c |

--- a/src/HOL/Probability/Borel_Space.thy Wed Sep 14 10:55:07 2011 +0200 +++ b/src/HOL/Probability/Borel_Space.thy Wed Sep 14 10:08:52 2011 -0400 @@ -1414,7 +1414,7 @@ proof fix a have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})" - by (auto simp: less_SUP_iff SUPR_apply) + by (auto simp: less_SUP_iff SUP_apply) then show "?sup -` {a<..} \<inter> space M \<in> sets M" using assms by auto qed @@ -1427,7 +1427,7 @@ proof fix a have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})" - by (auto simp: INF_less_iff INFI_apply) + by (auto simp: INF_less_iff INF_apply) then show "?inf -` {..<a} \<inter> space M \<in> sets M" using assms by auto qed