Description: Define a function constructing Caratheodory measurable sets for a given outer measure. See carsgval for its value. Definition 1.11.2 of Bogachev p. 41. (Contributed by Thierry Arnoux, 17-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | df-carsg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ccarsg | |
|
1 | vm | |
|
2 | cvv | |
|
3 | va | |
|
4 | 1 | cv | |
5 | 4 | cdm | |
6 | 5 | cuni | |
7 | 6 | cpw | |
8 | ve | |
|
9 | 8 | cv | |
10 | 3 | cv | |
11 | 9 10 | cin | |
12 | 11 4 | cfv | |
13 | cxad | |
|
14 | 9 10 | cdif | |
15 | 14 4 | cfv | |
16 | 12 15 13 | co | |
17 | 9 4 | cfv | |
18 | 16 17 | wceq | |
19 | 18 8 7 | wral | |
20 | 19 3 7 | crab | |
21 | 1 2 20 | cmpt | |
22 | 0 21 | wceq | |