--- a/NEWS Tue Apr 17 22:35:48 2018 +0100
+++ b/NEWS Wed Apr 18 15:57:36 2018 +0100
@@ -209,6 +209,10 @@
choice operator. The dual of this property is also proved in
Hilbert_Choice.thy.
+* New syntax for the minimum/maximum of a function over a finite set:
+MIN x\<in>A. B and even MIN x. B (only useful for finite types), also
+MAX.
+
* Clarifed theorem names:
Min.antimono ~> Min.subset_imp
@@ -255,8 +259,9 @@
* HOL-Algebra: renamed (^) to [^]
-* Session HOL-Analysis: Moebius functions and the Riemann mapping
-theorem.
+* Session HOL-Analysis: Moebius functions, the Riemann mapping
+theorem, the Vitali covering theorem, change-of-variables results for
+integration and measures.
* Class linordered_semiring_1 covers zero_less_one also, ruling out
pathologic instances. Minor INCOMPATIBILITY.
--- a/src/HOL/Algebra/Congruence.thy Tue Apr 17 22:35:48 2018 +0100
+++ b/src/HOL/Algebra/Congruence.thy Wed Apr 18 15:57:36 2018 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Algebra/Congruence.thy
Author: Clemens Ballarin, started 3 January 2008
- Copyright: Clemens Ballarin
+ with thanks to Paulo Emílio de Vilhena
*)
theory Congruence
@@ -119,7 +119,7 @@
by (fast intro: elemI elim: elemE dest: subsetD)
lemma (in equivalence) mem_imp_elem [simp, intro]:
- "[| x \<in> A; x \<in> carrier S |] ==> x .\<in> A"
+ "\<lbrakk> x \<in> A; x \<in> carrier S \<rbrakk> \<Longrightarrow> x .\<in> A"
unfolding elem_def by blast
lemma set_eqI:
@@ -215,15 +215,11 @@
lemma (in equivalence) set_eq_sym [sym]:
assumes "A {.=} B"
- and "A \<subseteq> carrier S" "B \<subseteq> carrier S"
shows "B {.=} A"
using assms
unfolding set_eq_def elem_def
by fast
-(* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *)
-(* alternatively, could declare lemmas [trans] = ssubst [where 'a = "'a set"] *)
-
lemma (in equivalence) equal_set_eq_trans [trans]:
assumes AB: "A = B" and BC: "B {.=} C"
shows "A {.=} C"
@@ -234,7 +230,6 @@
shows "A {.=} C"
using AB BC by simp
-
lemma (in equivalence) set_eq_trans [trans]:
assumes AB: "A {.=} B" and BC: "B {.=} C"
and carr: "A \<subseteq> carrier S" "B \<subseteq> carrier S" "C \<subseteq> carrier S"
@@ -265,46 +260,46 @@
show "c .\<in> A" by simp
qed
-(* FIXME: generalise for insert *)
+lemma (in equivalence) set_eq_insert_aux:
+ assumes x: "x .= x'"
+ and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S"
+ shows "\<forall>a \<in> (insert x A). a .\<in> (insert x' A)"
+proof
+ fix a
+ show "a \<in> insert x A \<Longrightarrow> a .\<in> insert x' A"
+ proof cases
+ assume "a \<in> A"
+ thus "a .\<in> insert x' A"
+ using carr(3) by blast
+ next
+ assume "a \<in> insert x A" "a \<notin> A"
+ hence "a = x"
+ by blast
+ thus "a .\<in> insert x' A"
+ by (meson x elemI insertI1)
+ qed
+qed
-(*
lemma (in equivalence) set_eq_insert:
assumes x: "x .= x'"
- and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S"
- shows "insert x A {.=} insert x' A"
- unfolding set_eq_def elem_def
-apply rule
-apply rule
-apply (case_tac "xa = x")
-using x apply fast
-apply (subgoal_tac "xa \<in> A") prefer 2 apply fast
-apply (rule_tac x=xa in bexI)
-using carr apply (rule_tac refl) apply auto [1]
-apply safe
-*)
+ and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S"
+ shows "insert x A {.=} insert x' A"
+proof-
+ have "(\<forall>a \<in> (insert x A). a .\<in> (insert x' A)) \<and>
+ (\<forall>a \<in> (insert x' A). a .\<in> (insert x A))"
+ using set_eq_insert_aux carr x sym by blast
+ thus "insert x A {.=} insert x' A"
+ using set_eq_def by blast
+qed
lemma (in equivalence) set_eq_pairI:
assumes xx': "x .= x'"
and carr: "x \<in> carrier S" "x' \<in> carrier S" "y \<in> carrier S"
shows "{x, y} {.=} {x', y}"
-unfolding set_eq_def elem_def
-proof safe
- have "x' \<in> {x', y}" by fast
- with xx' show "\<exists>b\<in>{x', y}. x .= b" by fast
-next
- have "y \<in> {x', y}" by fast
- with carr show "\<exists>b\<in>{x', y}. y .= b" by fast
-next
- have "x \<in> {x, y}" by fast
- with xx'[symmetric] carr
- show "\<exists>a\<in>{x, y}. x' .= a" by fast
-next
- have "y \<in> {x, y}" by fast
- with carr show "\<exists>a\<in>{x, y}. y .= a" by fast
-qed
+ using assms set_eq_insert by simp
lemma (in equivalence) is_closedI:
- assumes closed: "!!x y. [| x .= y; x \<in> A; y \<in> carrier S |] ==> y \<in> A"
+ assumes closed: "\<And>x y. \<lbrakk>x .= y; x \<in> A; y \<in> carrier S\<rbrakk> \<Longrightarrow> y \<in> A"
and S: "A \<subseteq> carrier S"
shows "is_closed A"
unfolding eq_is_closed_def eq_closure_of_def elem_def
@@ -312,19 +307,19 @@
by (blast dest: closed sym)
lemma (in equivalence) closure_of_eq:
- "[| x .= x'; A \<subseteq> carrier S; x \<in> closure_of A; x \<in> carrier S; x' \<in> carrier S |] ==> x' \<in> closure_of A"
+ "\<lbrakk>x .= x'; A \<subseteq> carrier S; x \<in> closure_of A; x' \<in> carrier S\<rbrakk> \<Longrightarrow> x' \<in> closure_of A"
unfolding eq_closure_of_def elem_def
by (blast intro: trans sym)
lemma (in equivalence) is_closed_eq [dest]:
- "[| x .= x'; x \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S |] ==> x' \<in> A"
+ "\<lbrakk>x .= x'; x \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S\<rbrakk> \<Longrightarrow> x' \<in> A"
unfolding eq_is_closed_def
using closure_of_eq [where A = A]
by simp
lemma (in equivalence) is_closed_eq_rev [dest]:
- "[| x .= x'; x' \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S |] ==> x \<in> A"
- by (drule sym) (simp_all add: is_closed_eq)
+ "\<lbrakk>x .= x'; x' \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S\<rbrakk> \<Longrightarrow> x \<in> A"
+ by (meson subsetD eq_is_closed_def is_closed_eq sym)
lemma closure_of_closed [simp, intro]:
fixes S (structure)
@@ -334,81 +329,55 @@
lemma closure_of_memI:
fixes S (structure)
- assumes "a .\<in> A"
- and "a \<in> carrier S"
+ assumes "a .\<in> A" and "a \<in> carrier S"
shows "a \<in> closure_of A"
-unfolding eq_closure_of_def
-using assms
-by fast
+ by (simp add: assms eq_closure_of_def)
lemma closure_ofI2:
fixes S (structure)
- assumes "a .= a'"
- and "a' \<in> A"
- and "a \<in> carrier S"
+ assumes "a .= a'" and "a' \<in> A" and "a \<in> carrier S"
shows "a \<in> closure_of A"
-unfolding eq_closure_of_def elem_def
-using assms
-by fast
+ by (meson assms closure_of_memI elem_def)
lemma closure_of_memE:
fixes S (structure)
- assumes p: "a \<in> closure_of A"
- and r: "\<lbrakk>a \<in> carrier S; a .\<in> A\<rbrakk> \<Longrightarrow> P"
+ assumes "a \<in> closure_of A"
+ and "\<lbrakk>a \<in> carrier S; a .\<in> A\<rbrakk> \<Longrightarrow> P"
shows "P"
-proof -
- from p
- have acarr: "a \<in> carrier S"
- and "a .\<in> A"
- by (simp add: eq_closure_of_def)+
- thus "P" by (rule r)
-qed
+ using eq_closure_of_def assms by fastforce
lemma closure_ofE2:
fixes S (structure)
- assumes p: "a \<in> closure_of A"
- and r: "\<And>a'. \<lbrakk>a \<in> carrier S; a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
+ assumes "a \<in> closure_of A"
+ and "\<And>a'. \<lbrakk>a \<in> carrier S; a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
shows "P"
-proof -
- from p have acarr: "a \<in> carrier S" by (simp add: eq_closure_of_def)
+ by (meson closure_of_memE elemE assms)
- from p have "\<exists>a'\<in>A. a .= a'" by (simp add: eq_closure_of_def elem_def)
- from this obtain a'
- where "a' \<in> A" and "a .= a'" by auto
-
- from acarr and this
- show "P" by (rule r)
+lemma (in equivalence) closure_inclusion:
+ assumes "A \<subseteq> B"
+ shows "closure_of A \<subseteq> closure_of B"
+ unfolding eq_closure_of_def
+proof
+ fix x
+ assume "x \<in> {y \<in> carrier S. y .\<in> A}"
+ hence "x \<in> carrier S \<and> x .\<in> A"
+ by blast
+ hence "x \<in> carrier S \<and> x .\<in> B"
+ using assms elem_subsetD by blast
+ thus "x \<in> {y \<in> carrier S. y .\<in> B}"
+ by simp
qed
-(*
-lemma (in equivalence) classes_consistent:
- assumes Acarr: "A \<subseteq> carrier S"
- shows "is_closed (closure_of A)"
-apply (blast intro: elemI elim elemE)
-using assms
-apply (intro is_closedI closure_of_memI, simp)
- apply (elim elemE closure_of_memE)
-proof -
- fix x a' a''
- assume carr: "x \<in> carrier S" "a' \<in> carrier S"
- assume a''A: "a'' \<in> A"
- with Acarr have "a'' \<in> carrier S" by fast
- note [simp] = carr this Acarr
-
- assume "x .= a'"
- also assume "a' .= a''"
- also from a''A
- have "a'' .\<in> A" by (simp add: elem_exact)
- finally show "x .\<in> A" by simp
-qed
-*)
-(*
lemma (in equivalence) classes_small:
assumes "is_closed B"
and "A \<subseteq> B"
shows "closure_of A \<subseteq> B"
-using assms
-by (blast dest: is_closedD2 elem_subsetD elim: closure_of_memE)
+proof-
+ have "closure_of A \<subseteq> closure_of B"
+ using closure_inclusion assms by simp
+ thus "closure_of A \<subseteq> B"
+ using assms(1) eq_is_closed_def by fastforce
+qed
lemma (in equivalence) classes_eq:
assumes "A \<subseteq> carrier S"
@@ -419,9 +388,21 @@
lemma (in equivalence) complete_classes:
assumes c: "is_closed A"
shows "A = closure_of A"
-using assms
-by (blast intro: closure_of_memI elem_exact dest: is_closedD1 is_closedD2 closure_of_memE)
-*)
+ using assms by (simp add: eq_is_closed_def)
+
+lemma (in equivalence) closure_idemp_weak:
+ "closure_of (closure_of A) {.=} closure_of A"
+ by (simp add: classes_eq set_eq_sym)
+
+lemma (in equivalence) closure_idemp_strong:
+ assumes "A \<subseteq> carrier S"
+ shows "closure_of (closure_of A) = closure_of A"
+ using assms closure_of_eq complete_classes is_closedI by auto
+
+lemma (in equivalence) complete_classes2:
+ assumes "A \<subseteq> carrier S"
+ shows "is_closed (closure_of A)"
+ using closure_idemp_strong by (simp add: assms eq_is_closed_def)
lemma equivalence_subset:
assumes "equivalence L" "A \<subseteq> carrier L"
--- a/src/HOL/Analysis/Change_Of_Vars.thy Tue Apr 17 22:35:48 2018 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Wed Apr 18 15:57:36 2018 +0100
@@ -1,12 +1,12 @@
theory Change_Of_Vars
- imports "HOL-Analysis.Vitali_Covering_Theorem" "HOL-Analysis.Determinants"
+ imports Vitali_Covering_Theorem Determinants
begin
subsection\<open>Induction on matrix row operations\<close>
lemma induct_matrix_row_operations:
- fixes P :: "(real^'n, 'n::finite) vec \<Rightarrow> bool"
+ fixes P :: "real^'n^'n \<Rightarrow> bool"
assumes zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A $ i $ Fun.swap m n id j)"
@@ -115,7 +115,7 @@
qed
lemma induct_matrix_elementary:
- fixes P :: "(real^'n, 'n::finite) vec \<Rightarrow> bool"
+ fixes P :: "real^'n^'n \<Rightarrow> bool"
assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
@@ -146,7 +146,7 @@
qed
lemma induct_matrix_elementary_alt:
- fixes P :: "(real^'n, 'n::finite) vec \<Rightarrow> bool"
+ fixes P :: "real^'n^'n \<Rightarrow> bool"
assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
@@ -196,14 +196,14 @@
then show "P (( *v) (A ** B))"
by (metis (no_types, lifting) comp linear_compose matrix_compose matrix_eq matrix_vector_mul matrix_vector_mul_linear)
next
- fix A :: "((real, 'n) vec, 'n) vec" and i
+ fix A :: "real^'n^'n" and i
assume "row i A = 0"
then show "P (( *v) A)"
by (metis inner_zero_left matrix_vector_mul_component matrix_vector_mul_linear row_def vec_eq_iff vec_lambda_beta zeroes)
next
- fix A :: "((real, 'n) vec, 'n) vec"
+ fix A :: "real^'n^'n"
assume 0: "\<And>i j. i \<noteq> j \<Longrightarrow> A $ i $ j = 0"
- have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x :: "(real, 'n) vec" and i :: "'n"
+ have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x and i :: "'n"
by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i])
then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = (( *v) A)"
by (auto simp: 0 matrix_vector_mult_def)
@@ -214,7 +214,7 @@
assume "m \<noteq> n"
have eq: "(\<Sum>j\<in>UNIV. if i = Fun.swap m n id j then x $ j else 0) =
(\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
- for i and x :: "(real, 'n) vec"
+ for i and x :: "real^'n"
unfolding swap_def by (rule sum.cong) auto
have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = (( *v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
@@ -223,7 +223,7 @@
next
fix m n :: "'n"
assume "m \<noteq> n"
- then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "(real, 'n) vec"
+ then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "real^'n"
by (auto simp: of_bool_def if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
then have "(\<lambda>x::real^'n. \<chi> i. if i = m then x $ m + x $ n else x $ i) =
(( *v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
@@ -390,7 +390,7 @@
using True by auto
have "ball 0 B \<subseteq> (\<lambda>x. \<chi> k. x $ k / m k) ` ball 0 ?C"
proof clarsimp
- fix x :: "(real, 'n) vec"
+ fix x :: "real^'n"
assume x: "norm x < B"
have [simp]: "\<bar>Max (range (\<lambda>k. \<bar>m k\<bar>))\<bar> = Max (range (\<lambda>k. \<bar>m k\<bar>))"
by (meson Max_ge abs_ge_zero abs_of_nonneg finite finite_imageI order_trans rangeI)
@@ -452,8 +452,6 @@
-
-
proposition
fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
assumes "linear f" "S \<in> lmeasurable"
@@ -473,7 +471,7 @@
using f [OF gS] g [OF S] matrix_compose [OF \<open>linear g\<close> \<open>linear f\<close>]
by (simp add: o_def image_comp abs_mult det_mul)
next
- fix f :: "(real, 'n) vec \<Rightarrow> (real, 'n) vec" and i and S :: "(real, 'n) vec set"
+ fix f :: "real^'n::_ \<Rightarrow> real^'n::_" and i and S :: "(real^'n::_) set"
assume "linear f" and 0: "\<And>x. f x $ i = 0" and "S \<in> lmeasurable"
then have "\<not> inj f"
by (metis (full_types) linear_injective_imp_surjective one_neq_zero surjE vec_component)
@@ -490,7 +488,7 @@
finally show "?Q f S" .
qed
next
- fix c and S :: "(real, 'n) vec set"
+ fix c and S :: "(real^'n::_) set"
assume "S \<in> lmeasurable"
show "(\<lambda>a. \<chi> i. c i * a $ i) ` S \<in> lmeasurable \<and> ?Q (\<lambda>a. \<chi> i. c i * a $ i) S"
proof
@@ -532,7 +530,7 @@
using measure_linear_sufficient [OF lin \<open>S \<in> lmeasurable\<close>] meq 1 by force+
qed
next
- fix m :: "'n" and n :: "'n" and S :: "(real, 'n) vec set"
+ fix m n :: "'n" and S :: "(real, 'n) vec set"
assume "m \<noteq> n" and "S \<in> lmeasurable"
let ?h = "\<lambda>v::(real, 'n) vec. \<chi> i. if i = m then v $ m + v $ n else v $ i"
have lin: "linear ?h"
@@ -616,26 +614,6 @@
by (simp add: measure_linear_image \<open>linear f\<close> S f)
qed
-lemma sets_lebesgue_inner_closed:
- assumes "S \<in> sets lebesgue" "e > 0"
- obtains T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "measure lebesgue (S - T) < e"
-proof -
- have "-S \<in> sets lebesgue"
- using assms by (simp add: Compl_in_sets_lebesgue)
- then obtain T where "open T" "-S \<subseteq> T"
- and T: "(T - -S) \<in> lmeasurable" "measure lebesgue (T - -S) < e"
- using lmeasurable_outer_open assms by blast
- show thesis
- proof
- show "closed (-T)"
- using \<open>open T\<close> by blast
- show "-T \<subseteq> S"
- using \<open>- S \<subseteq> T\<close> by auto
- show "S - ( -T) \<in> lmeasurable" "measure lebesgue (S - (- T)) < e"
- using T by (auto simp: Int_commute)
- qed
-qed
-
subsection\<open>@{text F_sigma} and @{text G_delta} sets.\<close>
(*https://en.wikipedia.org/wiki/F\<sigma>_set*)
@@ -645,7 +623,6 @@
inductive gdelta :: "'a::topological_space set \<Rightarrow> bool" where
"(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (INTER UNIV F)"
-
lemma fsigma_Union_compact:
fixes S :: "'a::{real_normed_vector,heine_borel} set"
shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = UNION UNIV F)"
@@ -698,12 +675,9 @@
by (simp add: 1 gdelta.intros open_closed)
qed
-
-
lemma gdelta_complement: "gdelta(- S) \<longleftrightarrow> fsigma S"
using fsigma_imp_gdelta gdelta_imp_fsigma by force
-
text\<open>A Lebesgue set is almost an @{text F_sigma} or @{text G_delta}.\<close>
lemma lebesgue_set_almost_fsigma:
assumes "S \<in> sets lebesgue"
@@ -1839,7 +1813,7 @@
using \<open>r > 0\<close> \<open>d > 0\<close> by auto
show "{x' \<in> S. \<exists>v. v \<noteq> 0 \<and> (\<forall>\<xi>>0. \<exists>e>0. \<forall>z\<in>S - {x'}. norm (x' - z) < e \<longrightarrow> \<bar>v \<bullet> (z - x')\<bar> < \<xi> * norm (x' - z))} \<inter> ball x (min d r) \<subseteq> ?W"
proof (clarsimp simp: dist_norm norm_minus_commute)
- fix y :: "(real, 'm) vec" and w :: "(real, 'm) vec"
+ fix y w
assume "y \<in> S" "w \<noteq> 0"
and less [rule_format]:
"\<forall>\<xi>>0. \<exists>e>0. \<forall>z\<in>S - {y}. norm (y - z) < e \<longrightarrow> \<bar>w \<bullet> (z - y)\<bar> < \<xi> * norm (y - z)"
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Tue Apr 17 22:35:48 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Wed Apr 18 15:57:36 2018 +0100
@@ -1297,6 +1297,26 @@
qed
qed
+lemma sets_lebesgue_inner_closed:
+ assumes "S \<in> sets lebesgue" "e > 0"
+ obtains T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "measure lebesgue (S - T) < e"
+proof -
+ have "-S \<in> sets lebesgue"
+ using assms by (simp add: Compl_in_sets_lebesgue)
+ then obtain T where "open T" "-S \<subseteq> T"
+ and T: "(T - -S) \<in> lmeasurable" "measure lebesgue (T - -S) < e"
+ using lmeasurable_outer_open assms by blast
+ show thesis
+ proof
+ show "closed (-T)"
+ using \<open>open T\<close> by blast
+ show "-T \<subseteq> S"
+ using \<open>- S \<subseteq> T\<close> by auto
+ show "S - ( -T) \<in> lmeasurable" "measure lebesgue (S - (- T)) < e"
+ using T by (auto simp: Int_commute)
+ 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)