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* = ( 𝑥 ∈ 𝒫 ℝ ↦ inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } , ℝ* , < ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		covol	⊢ vol*
1		vx	⊢ 𝑥
2		cr	⊢ ℝ
3	2	cpw	⊢ 𝒫 ℝ
4		vy	⊢ 𝑦
5		cxr	⊢ ℝ*
6		vf	⊢ 𝑓
7		cle	⊢ ≤
8	2 2	cxp	⊢ ( ℝ × ℝ )
9	7 8	cin	⊢ ( ≤ ∩ ( ℝ × ℝ ) )
10		cmap	⊢ ↑m
11		cn	⊢ ℕ
12	9 11 10	co	⊢ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ )
13	1	cv	⊢ 𝑥
14		cioo	⊢ (,)
15	6	cv	⊢ 𝑓
16	14 15	ccom	⊢ ( (,) ∘ 𝑓 )
17	16	crn	⊢ ran ( (,) ∘ 𝑓 )
18	17	cuni	⊢ ∪ ran ( (,) ∘ 𝑓 )
19	13 18	wss	⊢ 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 )
20	4	cv	⊢ 𝑦
21		c1	⊢ 1
22		caddc	⊢ +
23		cabs	⊢ abs
24		cmin	⊢ −
25	23 24	ccom	⊢ ( abs ∘ − )
26	25 15	ccom	⊢ ( ( abs ∘ − ) ∘ 𝑓 )
27	22 26 21	cseq	⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) )
28	27	crn	⊢ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) )
29		clt	⊢ <
30	28 5 29	csup	⊢ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < )
31	20 30	wceq	⊢ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < )
32	19 31	wa	⊢ ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) )
33	32 6 12	wrex	⊢ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) )
34	33 4 5	crab	⊢ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
35	34 5 29	cinf	⊢ inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } , ℝ* , < )
36	1 3 35	cmpt	⊢ ( 𝑥 ∈ 𝒫 ℝ ↦ inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } , ℝ* , < ) )
37	0 36	wceq	⊢ vol* = ( 𝑥 ∈ 𝒫 ℝ ↦ inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } , ℝ* , < ) )