src/HOL/Probability/Fin_Map.thy
changeset 50091 b3b5dc2350b7
parent 50088 32d1795cc77a
child 50094 84ddcf5364b4
equal deleted inserted replaced
50090:01203193dfa0 50091:b3b5dc2350b7
     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 sigma-algebra
    13   stay close to the developments of (finite) products @{const Pi\<^isub>E} and their sigma-algebra
    14   @{const Pi\<^isub>M}. *}
    14   @{const Pi\<^isub>M}. *}