Metamath Proof Explorer


Definition df-carsg

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 toCaraSiga=mVa𝒫domm|e𝒫dommmea+𝑒mea=me

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccarsg classtoCaraSiga
1 vm setvarm
2 cvv classV
3 va setvara
4 1 cv setvarm
5 4 cdm classdomm
6 5 cuni classdomm
7 6 cpw class𝒫domm
8 ve setvare
9 8 cv setvare
10 3 cv setvara
11 9 10 cin classea
12 11 4 cfv classmea
13 cxad class+𝑒
14 9 10 cdif classea
15 14 4 cfv classmea
16 12 15 13 co classmea+𝑒mea
17 9 4 cfv classme
18 16 17 wceq wffmea+𝑒mea=me
19 18 8 7 wral wffe𝒫dommmea+𝑒mea=me
20 19 3 7 crab classa𝒫domm|e𝒫dommmea+𝑒mea=me
21 1 2 20 cmpt classmVa𝒫domm|e𝒫dommmea+𝑒mea=me
22 0 21 wceq wfftoCaraSiga=mVa𝒫domm|e𝒫dommmea+𝑒mea=me