equal
deleted
inserted
replaced
1 (* Author: Johannes Hölzl <hoelzl@in.tum.de> *) |
1 (* Author: Johannes Hölzl <hoelzl@in.tum.de> *) |
2 |
2 |
3 section \<open>The Category of Measurable Spaces is not Cartesian Closed\<close> |
3 section \<open>The Category of Measurable Spaces is not Cartesian Closed\<close> |
4 |
4 |
5 theory Measure_Not_CCC |
5 theory Measure_Not_CCC |
6 imports Probability |
6 imports "HOL-Probability.Probability" |
7 begin |
7 begin |
8 |
8 |
9 text \<open> |
9 text \<open> |
10 We show that the category of measurable spaces with measurable functions as morphisms is not a |
10 We show that the category of measurable spaces with measurable functions as morphisms is not a |
11 Cartesian closed category. While the category has products and terminal objects, the exponential |
11 Cartesian closed category. While the category has products and terminal objects, the exponential |