equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 section \<open>Finite Maps\<close> |
5 section \<open>Finite Maps\<close> |
6 |
6 |
7 theory Fin_Map |
7 theory Fin_Map |
8 imports "~~/src/HOL/Analysis/Finite_Product_Measure" "~~/src/HOL/Library/Finite_Map" |
8 imports "HOL-Analysis.Finite_Product_Measure" "HOL-Library.Finite_Map" |
9 begin |
9 begin |
10 |
10 |
11 text \<open>The @{type fmap} type can be instantiated to @{class polish_space}, needed for the proof of |
11 text \<open>The @{type fmap} type can be instantiated to @{class polish_space}, needed for the proof of |
12 projective limit. @{const extensional} functions are used for the representation in order to |
12 projective limit. @{const extensional} functions are used for the representation in order to |
13 stay close to the developments of (finite) products @{const Pi\<^sub>E} and their sigma-algebra |
13 stay close to the developments of (finite) products @{const Pi\<^sub>E} and their sigma-algebra |