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

Step	Hyp	Ref	Expression
1		covol 23038	. 2 class vol*
2		vx	. . 3 setvar 𝑥
3		cr 9814	. . . 4 class ℝ
4	3	cpw 4108	. . 3 class 𝒫 ℝ
5	2	cv 1474	. . . . . . . 8 class 𝑥
6		cioo 12046	. . . . . . . . . . 11 class (,)
7		vf	. . . . . . . . . . . 12 setvar 𝑓
8	7	cv 1474	. . . . . . . . . . 11 class 𝑓
9	6, 8	ccom 5042	. . . . . . . . . 10 class ((,) ∘ 𝑓)
10	9	crn 5039	. . . . . . . . 9 class ran ((,) ∘ 𝑓)
11	10	cuni 4372	. . . . . . . 8 class ∪ ran ((,) ∘ 𝑓)
12	5, 11	wss 3540	. . . . . . 7 wff 𝑥 ⊆ ∪ ran ((,) ∘ 𝑓)
13		vy	. . . . . . . . 9 setvar 𝑦
14	13	cv 1474	. . . . . . . 8 class 𝑦
15		caddc 9818	. . . . . . . . . . 11 class +
16		cabs 13822	. . . . . . . . . . . . 13 class abs
17		cmin 10145	. . . . . . . . . . . . 13 class −
18	16, 17	ccom 5042	. . . . . . . . . . . 12 class (abs ∘ − )
19	18, 8	ccom 5042	. . . . . . . . . . 11 class ((abs ∘ − ) ∘ 𝑓)
20		c1 9816	. . . . . . . . . . 11 class 1
21	15, 19, 20	cseq 12663	. . . . . . . . . 10 class seq1( + , ((abs ∘ − ) ∘ 𝑓))
22	21	crn 5039	. . . . . . . . 9 class ran seq1( + , ((abs ∘ − ) ∘ 𝑓))
23		cxr 9952	. . . . . . . . 9 class ℝ*
24		clt 9953	. . . . . . . . 9 class <
25	22, 23, 24	csup 8229	. . . . . . . 8 class sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )
26	14, 25	wceq 1475	. . . . . . 7 wff 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )
27	12, 26	wa 383	. . . . . 6 wff (𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
28		cle 9954	. . . . . . . 8 class ≤
29	3, 3	cxp 5036	. . . . . . . 8 class (ℝ × ℝ)
30	28, 29	cin 3539	. . . . . . 7 class ( ≤ ∩ (ℝ × ℝ))
31		cn 10897	. . . . . . 7 class ℕ
32		cmap 7744	. . . . . . 7 class ↑𝑚
33	30, 31, 32	co 6549	. . . . . 6 class (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)
34	27, 7, 33	wrex 2897	. . . . 5 wff ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))
35	34, 13, 23	crab 2900	. . . 4 class {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}
36	35, 23, 24	cinf 8230	. . 3 class inf({𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < )
37	2, 4, 36	cmpt 4643	. 2 class (𝑥 ∈ 𝒫 ℝ ↦ inf({𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))
38	1, 37	wceq 1475	1 wff vol* = (𝑥 ∈ 𝒫 ℝ ↦ inf({𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))

This definition is referenced by:  ovolval  23049  ovolf  23057