summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Fin_Map.thy

changeset 50091 | b3b5dc2350b7 |

parent 50088 | 32d1795cc77a |

child 50094 | 84ddcf5364b4 |

1.1 --- a/src/HOL/Probability/Fin_Map.thy Thu Nov 15 16:07:52 2012 +0100 1.2 +++ b/src/HOL/Probability/Fin_Map.thy Thu Nov 15 17:36:08 2012 +0100 1.3 @@ -1,13 +1,13 @@ 1.4 -(* Title: HOL/Probability/Projective_Family.thy 1.5 +(* Title: HOL/Probability/Fin_Map.thy 1.6 Author: Fabian Immler, TU München 1.7 *) 1.8 1.9 +header {* Finite Maps *} 1.10 + 1.11 theory Fin_Map 1.12 imports Finite_Product_Measure 1.13 begin 1.14 1.15 -section {* Finite Maps *} 1.16 - 1.17 text {* Auxiliary type that is instantiated to @{class polish_space}, needed for the proof of 1.18 projective limit. @{const extensional} functions are used for the representation in order to 1.19 stay close to the developments of (finite) products @{const Pi\<^isub>E} and their sigma-algebra