equal
deleted
inserted
replaced
1 (* Title: HOL/Probability/Projective_Family.thy 
1 (* Title: HOL/Probability/Fin_Map.thy 
2 Author: Fabian Immler, TU München 
2 Author: Fabian Immler, TU München 
3 *) 
3 *) 

4 

5 header {* Finite Maps *} 
4 
6 
5 theory Fin_Map 
7 theory Fin_Map 
6 imports Finite_Product_Measure 
8 imports Finite_Product_Measure 
7 begin 
9 begin 
8 

9 section {* Finite Maps *} 

10 
10 
11 text {* Auxiliary type that is instantiated to @{class polish_space}, needed for the proof of 
11 text {* Auxiliary type that is 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\<^isub>E} and their sigmaalgebra 
13 stay close to the developments of (finite) products @{const Pi\<^isub>E} and their sigmaalgebra 
14 @{const Pi\<^isub>M}. *} 
14 @{const Pi\<^isub>M}. *} 