equal
deleted
inserted
replaced
318 locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2 |
318 locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2 |
319 for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme" |
319 for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme" |
320 |
320 |
321 sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2 |
321 sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2 |
322 by default |
322 by default |
323 |
|
324 lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B" |
|
325 proof |
|
326 fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B" |
|
327 by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros) |
|
328 qed |
|
329 |
323 |
330 lemma (in pair_sigma_finite) measure_cut_measurable_fst: |
324 lemma (in pair_sigma_finite) measure_cut_measurable_fst: |
331 assumes "Q \<in> sets P" shows "(\<lambda>x. measure M2 (Pair x -` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _") |
325 assumes "Q \<in> sets P" shows "(\<lambda>x. measure M2 (Pair x -` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _") |
332 proof - |
326 proof - |
333 have [intro]: "sigma_algebra M1" and [intro]: "sigma_algebra M2" by default+ |
327 have [intro]: "sigma_algebra M1" and [intro]: "sigma_algebra M2" by default+ |