equal
deleted
inserted
replaced
588 qed simp_all |
588 qed simp_all |
589 |
589 |
590 lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))" |
590 lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))" |
591 proof - |
591 proof - |
592 have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)" |
592 have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)" |
593 unfolding SUPR_def image_compose |
593 unfolding SUP_def image_compose |
594 unfolding surj_from_nat .. |
594 unfolding surj_from_nat .. |
595 then show ?thesis by simp |
595 then show ?thesis by simp |
596 qed |
596 qed |
597 |
597 |
598 lemma (in measure_space) null_sets_UN[intro]: |
598 lemma (in measure_space) null_sets_UN[intro]: |