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 ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } )