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 30704
Description: Define a function constructing Caratheodory measurable sets for a given outer measure. See carsgval 30705 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 30703 . 2 class toCaraSiga
2 vm . . 3 setvar 𝑚
3 cvv 3351 . . 3 class V
4 ve . . . . . . . . . 10 setvar 𝑒
54cv 1630 . . . . . . . . 9 class 𝑒
6 va . . . . . . . . . 10 setvar 𝑎
76cv 1630 . . . . . . . . 9 class 𝑎
85, 7cin 3722 . . . . . . . 8 class (𝑒𝑎)
92cv 1630 . . . . . . . 8 class 𝑚
108, 9cfv 6031 . . . . . . 7 class (𝑚‘(𝑒𝑎))
115, 7cdif 3720 . . . . . . . 8 class (𝑒𝑎)
1211, 9cfv 6031 . . . . . . 7 class (𝑚‘(𝑒𝑎))
13 cxad 12149 . . . . . . 7 class +𝑒
1410, 12, 13co 6793 . . . . . 6 class ((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎)))
155, 9cfv 6031 . . . . . 6 class (𝑚𝑒)
1614, 15wceq 1631 . . . . 5 wff ((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)
179cdm 5249 . . . . . . 7 class dom 𝑚
1817cuni 4574 . . . . . 6 class dom 𝑚
1918cpw 4297 . . . . 5 class 𝒫 dom 𝑚
2016, 4, 19wral 3061 . . . 4 wff 𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)
2120, 6, 19crab 3065 . . 3 class {𝑎 ∈ 𝒫 dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)}
222, 3, 21cmpt 4863 . 2 class (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)})
231, 22wceq 1631 1 wff toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)})
Colors of variables: wff setvar class
This definition is referenced by:  carsgval  30705
  Copyright terms: Public domain W3C validator