Metamath Proof Explorer

Definition df-ovol

Description: Define the outer Lebesgue measure for subsets of the reals. Here f is a function from the positive integers to pairs <. a , b >. with a <_ b , and the outer volume of the set x is the infimum over all such functions such that the union of the open intervals ( a , b ) covers x of the sum of b - a . (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 17-Sep-2020)

Ref Expression
Assertion df-ovol ⊢ vol * = x ∈ 𝒫 ℝ ⟼ sup y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ℝ * <

Detailed syntax breakdown

Step Hyp Ref Expression
0 covol class vol *
1 vx setvar x
2 cr class ℝ
3 2 cpw class 𝒫 ℝ
4 vy setvar y
5 cxr class ℝ *
6 vf setvar f
7 cle class ≤
8 2 2 cxp class ℝ 2
9 7 8 cin class ≤ ∩ ℝ 2
10 cmap class ↑ 𝑚
11 cn class ℕ
12 9 11 10 co class ≤ ∩ ℝ 2 ℕ
13 1 cv setvar x
14 cioo class .
15 6 cv setvar f
16 14 15 ccom class . ∘ f
17 16 crn class ran ⁡ . ∘ f
18 17 cuni class ⋃ ran ⁡ . ∘ f
19 13 18 wss wff x ⊆ ⋃ ran ⁡ . ∘ f
20 4 cv setvar y
21 c1 class 1
22 caddc class +
23 cabs class abs
24 cmin class −
25 23 24 ccom class abs ∘ −
26 25 15 ccom class abs ∘ − ∘ f
27 22 26 21 cseq class seq 1 + abs ∘ − ∘ f
28 27 crn class ran ⁡ seq 1 + abs ∘ − ∘ f
29 clt class <
30 28 5 29 csup class sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
31 20 30 wceq wff y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
32 19 31 wa wff x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
33 32 6 12 wrex wff ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
34 33 4 5 crab class y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
35 34 5 29 cinf class sup y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ℝ * <
36 1 3 35 cmpt class x ∈ 𝒫 ℝ ⟼ sup y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ℝ * <
37 0 36 wceq wff vol * = x ∈ 𝒫 ℝ ⟼ sup y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ℝ * <