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	$$⊢\underset{u}{⇝}=\left(s\in \mathrm{V}⟼\left\{⟨f,y⟩|\exists n\in \mathbb{Z}\left(f:{\mathbb{Z}}_{\ge n}⟶{ℂ}^s\wedge y:s⟶ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in s\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|<x\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		culm	$$class\underset{u}{⇝}$$
1		vs	$$setvars$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		vy	$$setvary$$
5		vn	$$setvarn$$
6		cz	$$class\mathbb{Z}$$
7	3	cv	$$setvarf$$
8		cuz	$$class{\mathbb{Z}}_{\ge }$$
9	5	cv	$$setvarn$$
10	9 8	cfv	$$class{\mathbb{Z}}_{\ge n}$$
11		cc	$$classℂ$$
12		cmap	$$class{\uparrow }_{𝑚}$$
13	1	cv	$$setvars$$
14	11 13 12	co	$$class\left({ℂ}^s\right)$$
15	10 14 7	wf	$$wfff:{\mathbb{Z}}_{\ge n}⟶{ℂ}^s$$
16	4	cv	$$setvary$$
17	13 11 16	wf	$$wffy:s⟶ℂ$$
18		vx	$$setvarx$$
19		crp	$$class{ℝ}^{+}$$
20		vj	$$setvarj$$
21		vk	$$setvark$$
22	20	cv	$$setvarj$$
23	22 8	cfv	$$class{\mathbb{Z}}_{\ge j}$$
24		vz	$$setvarz$$
25		cabs	$$class\mathrm{abs}$$
26	21	cv	$$setvark$$
27	26 7	cfv	$$classf\left(k\right)$$
28	24	cv	$$setvarz$$
29	28 27	cfv	$$classf\left(k\right)\left(z\right)$$
30		cmin	$$class-$$
31	28 16	cfv	$$classy\left(z\right)$$
32	29 31 30	co	$$class\left(f\left(k\right)\left(z\right)-y\left(z\right)\right)$$
33	32 25	cfv	$$class\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|$$
34		clt	$$class<$$
35	18	cv	$$setvarx$$
36	33 35 34	wbr	$$wff\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|<x$$
37	36 24 13	wral	$$wff\forall z\in s\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|<x$$
38	37 21 23	wral	$$wff\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in s\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|<x$$
39	38 20 10	wrex	$$wff\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in s\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|<x$$
40	39 18 19	wral	$$wff\forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in s\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|<x$$
41	15 17 40	w3a	$$wff\left(f:{\mathbb{Z}}_{\ge n}⟶{ℂ}^s\wedge y:s⟶ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in s\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|<x\right)$$
42	41 5 6	wrex	$$wff\exists n\in \mathbb{Z}\left(f:{\mathbb{Z}}_{\ge n}⟶{ℂ}^s\wedge y:s⟶ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in s\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|<x\right)$$
43	42 3 4	copab	$$class\left\{⟨f,y⟩|\exists n\in \mathbb{Z}\left(f:{\mathbb{Z}}_{\ge n}⟶{ℂ}^s\wedge y:s⟶ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in s\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|<x\right)\right\}$$
44	1 2 43	cmpt	$$class\left(s\in \mathrm{V}⟼\left\{⟨f,y⟩|\exists n\in \mathbb{Z}\left(f:{\mathbb{Z}}_{\ge n}⟶{ℂ}^s\wedge y:s⟶ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in s\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|<x\right)\right\}\right)$$
45	0 44	wceq	$$wff\underset{u}{⇝}=\left(s\in \mathrm{V}⟼\left\{⟨f,y⟩|\exists n\in \mathbb{Z}\left(f:{\mathbb{Z}}_{\ge n}⟶{ℂ}^s\wedge y:s⟶ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in s\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|<x\right)\right\}\right)$$