src/HOL/Probability/Borel_Space.thy
changeset 45287 97df8c08291c
parent 44928 7ef6505bde7f
child 45288 fc3c7db5bb2f
equal deleted inserted replaced
45286:23e1899503ee 45287:97df8c08291c
     4 *)
     4 *)
     5 
     5 
     6 header {*Borel spaces*}
     6 header {*Borel spaces*}
     7 
     7 
     8 theory Borel_Space
     8 theory Borel_Space
     9   imports Sigma_Algebra Multivariate_Analysis
     9   imports Sigma_Algebra "~~/src/HOL/Multvariate_Analysis/Multivariate_Analysis"
    10 begin
    10 begin
    11 
    11 
    12 section "Generic Borel spaces"
    12 section "Generic Borel spaces"
    13 
    13 
    14 definition "borel = sigma \<lparr> space = UNIV::'a::topological_space set, sets = {S. open S}\<rparr>"
    14 definition "borel = sigma \<lparr> space = UNIV::'a::topological_space set, sets = {S. open S}\<rparr>"