Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-carsg Structured version   Visualization version   GIF version

Definition df-carsg 29525
Description: Define a function constructing Caratheodory measurable sets for a given outer measure. See carsgval 29526 for its value. Definition 1.11.2 of [Bogachev] p. 41. (Contributed by Thierry Arnoux, 17-May-2020.)
Assertion
Ref Expression
df-carsg toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)})
Distinct variable group:   𝑚,𝑎,𝑒

Detailed syntax breakdown of Definition df-carsg
StepHypRef Expression
1 ccarsg 29524 . 2 class toCaraSiga
2 vm . . 3 setvar 𝑚
3 cvv 3172 . . 3 class V
4 ve . . . . . . . . . 10 setvar 𝑒
54cv 1473 . . . . . . . . 9 class 𝑒
6 va . . . . . . . . . 10 setvar 𝑎
76cv 1473 . . . . . . . . 9 class 𝑎
85, 7cin 3538 . . . . . . . 8 class (𝑒𝑎)
92cv 1473 . . . . . . . 8 class 𝑚
108, 9cfv 5790 . . . . . . 7 class (𝑚‘(𝑒𝑎))
115, 7cdif 3536 . . . . . . . 8 class (𝑒𝑎)
1211, 9cfv 5790 . . . . . . 7 class (𝑚‘(𝑒𝑎))
13 cxad 11779 . . . . . . 7 class +𝑒
1410, 12, 13co 6527 . . . . . 6 class ((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎)))
155, 9cfv 5790 . . . . . 6 class (𝑚𝑒)
1614, 15wceq 1474 . . . . 5 wff ((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)
179cdm 5028 . . . . . . 7 class dom 𝑚
1817cuni 4366 . . . . . 6 class dom 𝑚
1918cpw 4107 . . . . 5 class 𝒫 dom 𝑚
2016, 4, 19wral 2895 . . . 4 wff 𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)
2120, 6, 19crab 2899 . . 3 class {𝑎 ∈ 𝒫 dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)}
222, 3, 21cmpt 4637 . 2 class (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)})
231, 22wceq 1474 1 wff toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)})
Colors of variables: wff setvar class
This definition is referenced by:  carsgval  29526
  Copyright terms: Public domain W3C validator