equal
deleted
inserted
replaced
95 measurable_comp[measurable (raw)] |
95 measurable_comp[measurable (raw)] |
96 measurable_sets[measurable (raw)] |
96 measurable_sets[measurable (raw)] |
97 |
97 |
98 declare measurable_cong_sets[measurable_cong] |
98 declare measurable_cong_sets[measurable_cong] |
99 declare sets_restrict_space_cong[measurable_cong] |
99 declare sets_restrict_space_cong[measurable_cong] |
|
100 declare sets_restrict_UNIV[measurable_cong] |
100 |
101 |
101 lemma predE[measurable (raw)]: |
102 lemma predE[measurable (raw)]: |
102 "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M" |
103 "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M" |
103 unfolding pred_def . |
104 unfolding pred_def . |
104 |
105 |