| changeset 33536 | fd28b7399f2b |
| parent 33533 | 40b44cb20c8c |
| child 37032 | 58a0757031dd |
| 33535:b233f48a4d3d | 33536:fd28b7399f2b |
|---|---|
233 lemma (in sigma_algebra) sigma_subset: |
233 lemma (in sigma_algebra) sigma_subset: |
234 "a \<subseteq> sets M ==> sets (sigma (space M) a) \<subseteq> (sets M)" |
234 "a \<subseteq> sets M ==> sets (sigma (space M) a) \<subseteq> (sets M)" |
235 by (simp add: sigma_def sigma_sets_subset) |
235 by (simp add: sigma_def sigma_sets_subset) |
236 |
236 |
237 end |
237 end |
238 |