--- a/src/HOL/Analysis/Lebesgue_Measure.thy Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Mon Feb 19 16:44:45 2018 +0000
@@ -1134,4 +1134,12 @@
qed
qed
+lemma lebesgue_openin:
+ "\<lbrakk>openin (subtopology euclidean S) T; S \<in> sets lebesgue\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
+ by (metis borel_open openin_open sets.Int sets_completionI_sets sets_lborel)
+
+lemma lebesgue_closedin:
+ "\<lbrakk>closedin (subtopology euclidean S) T; S \<in> sets lebesgue\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
+ by (metis borel_closed closedin_closed sets.Int sets_completionI_sets sets_lborel)
+
end