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

Metamath Proof Explorer

Definition df-ulm

Description: Define the uniform convergence of a sequence of functions. Here F ( ~>uS ) G if F is a sequence of functions F ( n ) , n e. NN defined on S and G is a function on S , and for every 0 < x there is a j such that the functions F ( k ) for j <_ k are all uniformly within x of G on the domain S . Compare with df-clim . (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Assertion df-ulm ⇝𝑢 = ( 𝑠 ∈ V ↦ { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ∧ 𝑦 : 𝑠 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 culm ⊢ ⇝𝑢
1 vs ⊢ 𝑠
2 cvv ⊢ V
3 vf ⊢ 𝑓
4 vy ⊢ 𝑦
5 vn ⊢ 𝑛
6 cz ⊢ ℤ
7 3 cv ⊢ 𝑓
8 cuz ⊢ ℤ≥
9 5 cv ⊢ 𝑛
10 9 8 cfv ⊢ ( ℤ≥ ‘ 𝑛 )
11 cc ⊢ ℂ
12 cmap ⊢ ↑m
13 1 cv ⊢ 𝑠
14 11 13 12 co ⊢ ( ℂ ↑m 𝑠 )
15 10 14 7 wf ⊢ 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 )
16 4 cv ⊢ 𝑦
17 13 11 16 wf ⊢ 𝑦 : 𝑠 ⟶ ℂ
18 vx ⊢ 𝑥
19 crp ⊢ ℝ+
20 vj ⊢ 𝑗
21 vk ⊢ 𝑘
22 20 cv ⊢ 𝑗
23 22 8 cfv ⊢ ( ℤ≥ ‘ 𝑗 )
24 vz ⊢ 𝑧
25 cabs ⊢ abs
26 21 cv ⊢ 𝑘
27 26 7 cfv ⊢ ( 𝑓 ‘ 𝑘 )
28 24 cv ⊢ 𝑧
29 28 27 cfv ⊢ ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 )
30 cmin ⊢ −
31 28 16 cfv ⊢ ( 𝑦 ‘ 𝑧 )
32 29 31 30 co ⊢ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) )
33 32 25 cfv ⊢ ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) )
34 clt ⊢ <
35 18 cv ⊢ 𝑥
36 33 35 34 wbr ⊢ ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥
37 36 24 13 wral ⊢ ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥
38 37 21 23 wral ⊢ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥
39 38 20 10 wrex ⊢ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥
40 39 18 19 wral ⊢ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥
41 15 17 40 w3a ⊢ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ∧ 𝑦 : 𝑠 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 )
42 41 5 6 wrex ⊢ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ∧ 𝑦 : 𝑠 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 )
43 42 3 4 copab ⊢ { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ∧ 𝑦 : 𝑠 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) }
44 1 2 43 cmpt ⊢ ( 𝑠 ∈ V ↦ { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ∧ 𝑦 : 𝑠 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } )
45 0 44 wceq ⊢ ⇝𝑢 = ( 𝑠 ∈ V ↦ { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ∧ 𝑦 : 𝑠 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } )