Description: The predicate " A is measurable w.r.t. the n-dimensional Lebesgue measure". A set is measurable if it splits every other set x in a "nice" way, that is, if the measure of the pieces x i^i A and x \ A sum up to the measure of x . Definition 114E of Fremlin1 p. 25. (Contributed by Glauco Siliprandi, 3-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | isvonmbl.1 | |
|
Assertion | isvonmbl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isvonmbl.1 | |
|
2 | 1 | dmvon | |
3 | 2 | eleq2d | |
4 | 1 | ovnome | |
5 | eqid | |
|
6 | 4 5 | caragenel | |
7 | elpwi | |
|
8 | 7 | adantl | |
9 | 1 | unidmovn | |
10 | 9 | adantr | |
11 | 8 10 | sseqtrd | |
12 | 11 | ex | |
13 | simpr | |
|
14 | 9 | eqcomd | |
15 | 14 | adantr | |
16 | 13 15 | sseqtrd | |
17 | ovex | |
|
18 | 17 | ssex | |
19 | elpwg | |
|
20 | 18 19 | syl | |
21 | 20 | adantl | |
22 | 16 21 | mpbird | |
23 | 22 | ex | |
24 | 12 23 | impbid | |
25 | 9 | pweqd | |
26 | raleq | |
|
27 | 25 26 | syl | |
28 | 24 27 | anbi12d | |
29 | 3 6 28 | 3bitrd | |