Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ovol Structured version   Visualization version   GIF version

Definition df-ovol 23040
 Description: Define the outer Lebesgue measure for subsets of the reals. Here 𝑓 is a function from the positive integers to pairs ⟨𝑎, 𝑏⟩ with 𝑎 ≤ 𝑏, and the outer volume of the set 𝑥 is the infimum over all such functions such that the union of the open intervals (𝑎, 𝑏) covers 𝑥 of the sum of 𝑏 − 𝑎. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 17-Sep-2020.)
Assertion
Ref Expression
df-ovol vol* = (𝑥 ∈ 𝒫 ℝ ↦ inf({𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑥 ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))
Distinct variable group:   𝑥,𝑦,𝑓

Detailed syntax breakdown of Definition df-ovol
StepHypRef Expression
1 covol 23038 . 2 class vol*
2 vx . . 3 setvar 𝑥
3 cr 9814 . . . 4 class
43cpw 4108 . . 3 class 𝒫 ℝ
52cv 1474 . . . . . . . 8 class 𝑥
6 cioo 12046 . . . . . . . . . . 11 class (,)
7 vf . . . . . . . . . . . 12 setvar 𝑓
87cv 1474 . . . . . . . . . . 11 class 𝑓
96, 8ccom 5042 . . . . . . . . . 10 class ((,) ∘ 𝑓)
109crn 5039 . . . . . . . . 9 class ran ((,) ∘ 𝑓)
1110cuni 4372 . . . . . . . 8 class ran ((,) ∘ 𝑓)
125, 11wss 3540 . . . . . . 7 wff 𝑥 ran ((,) ∘ 𝑓)
13 vy . . . . . . . . 9 setvar 𝑦
1413cv 1474 . . . . . . . 8 class 𝑦
15 caddc 9818 . . . . . . . . . . 11 class +
16 cabs 13822 . . . . . . . . . . . . 13 class abs
17 cmin 10145 . . . . . . . . . . . . 13 class
1816, 17ccom 5042 . . . . . . . . . . . 12 class (abs ∘ − )
1918, 8ccom 5042 . . . . . . . . . . 11 class ((abs ∘ − ) ∘ 𝑓)
20 c1 9816 . . . . . . . . . . 11 class 1
2115, 19, 20cseq 12663 . . . . . . . . . 10 class seq1( + , ((abs ∘ − ) ∘ 𝑓))
2221crn 5039 . . . . . . . . 9 class ran seq1( + , ((abs ∘ − ) ∘ 𝑓))
23 cxr 9952 . . . . . . . . 9 class *
24 clt 9953 . . . . . . . . 9 class <
2522, 23, 24csup 8229 . . . . . . . 8 class sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )
2614, 25wceq 1475 . . . . . . 7 wff 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )
2712, 26wa 383 . . . . . 6 wff (𝑥 ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
28 cle 9954 . . . . . . . 8 class
293, 3cxp 5036 . . . . . . . 8 class (ℝ × ℝ)
3028, 29cin 3539 . . . . . . 7 class ( ≤ ∩ (ℝ × ℝ))
31 cn 10897 . . . . . . 7 class
32 cmap 7744 . . . . . . 7 class 𝑚
3330, 31, 32co 6549 . . . . . 6 class (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)
3427, 7, 33wrex 2897 . . . . 5 wff 𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑥 ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
3534, 13, 23crab 2900 . . . 4 class {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑥 ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}
3635, 23, 24cinf 8230 . . 3 class inf({𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑥 ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < )
372, 4, 36cmpt 4643 . 2 class (𝑥 ∈ 𝒫 ℝ ↦ inf({𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑥 ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))
381, 37wceq 1475 1 wff vol* = (𝑥 ∈ 𝒫 ℝ ↦ inf({𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑥 ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))
 Colors of variables: wff setvar class This definition is referenced by:  ovolval  23049  ovolf  23057
 Copyright terms: Public domain W3C validator