equal
deleted
inserted
replaced
405 by (metis Compl_eq_Diff_UNIV double_compl space_borel space_completion space_lborel Sigma_Algebra.sets.compl_sets) |
405 by (metis Compl_eq_Diff_UNIV double_compl space_borel space_completion space_lborel Sigma_Algebra.sets.compl_sets) |
406 |
406 |
407 lemma measurable_lebesgue_cong: |
407 lemma measurable_lebesgue_cong: |
408 assumes "\<And>x. x \<in> S \<Longrightarrow> f x = g x" |
408 assumes "\<And>x. x \<in> S \<Longrightarrow> f x = g x" |
409 shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M" |
409 shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M" |
410 by (metis (mono_tags, lifting) IntD1 assms measurable_cong_strong space_restrict_space) |
410 by (metis (mono_tags, lifting) IntD1 assms measurable_cong_simp space_restrict_space) |
411 |
411 |
412 text%unimportant \<open>Measurability of continuous functions\<close> |
412 text%unimportant \<open>Measurability of continuous functions\<close> |
413 |
413 |
414 lemma continuous_imp_measurable_on_sets_lebesgue: |
414 lemma continuous_imp_measurable_on_sets_lebesgue: |
415 assumes f: "continuous_on S f" and S: "S \<in> sets lebesgue" |
415 assumes f: "continuous_on S f" and S: "S \<in> sets lebesgue" |