This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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* = ( 𝑥 ∈ 𝒫 ℝ ↦ 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 ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } , ℝ* , < ) )