Definition df-ulm 23935

Description: Define the uniform convergence of a sequence of functions. Here 𝐹(⇝_𝑢‘𝑆)𝐺 if 𝐹 is a sequence of functions 𝐹(𝑛), 𝑛 ∈ ℕ defined on 𝑆 and 𝐺 is a function on 𝑆, and for every 0 < 𝑥 there is a 𝑗 such that the functions 𝐹(𝑘) for 𝑗 ≤ 𝑘 are all uniformly within 𝑥 of 𝐺 on the domain 𝑆. Compare with df-clim 14067. (Contributed by Mario Carneiro, 26-Feb-2015.)

Assertion

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

Distinct variable group:   𝑓,𝑗,𝑘,𝑛,𝑠,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ulm

Step	Hyp	Ref	Expression
1		culm 23934	. 2 class ⇝𝑢
2		vs	. . 3 setvar 𝑠
3		cvv 3173	. . 3 class V
4		vn	. . . . . . . . 9 setvar 𝑛
5	4	cv 1474	. . . . . . . 8 class 𝑛
6		cuz 11563	. . . . . . . 8 class ℤ≥
7	5, 6	cfv 5804	. . . . . . 7 class (ℤ≥‘𝑛)
8		cc 9813	. . . . . . . 8 class ℂ
9	2	cv 1474	. . . . . . . 8 class 𝑠
10		cmap 7744	. . . . . . . 8 class ↑𝑚
11	8, 9, 10	co 6549	. . . . . . 7 class (ℂ ↑𝑚 𝑠)
12		vf	. . . . . . . 8 setvar 𝑓
13	12	cv 1474	. . . . . . 7 class 𝑓
14	7, 11, 13	wf 5800	. . . . . 6 wff 𝑓:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑠)
15		vy	. . . . . . . 8 setvar 𝑦
16	15	cv 1474	. . . . . . 7 class 𝑦
17	9, 8, 16	wf 5800	. . . . . 6 wff 𝑦:𝑠⟶ℂ
18		vz	. . . . . . . . . . . . . . 15 setvar 𝑧
19	18	cv 1474	. . . . . . . . . . . . . 14 class 𝑧
20		vk	. . . . . . . . . . . . . . . 16 setvar 𝑘
21	20	cv 1474	. . . . . . . . . . . . . . 15 class 𝑘
22	21, 13	cfv 5804	. . . . . . . . . . . . . 14 class (𝑓‘𝑘)
23	19, 22	cfv 5804	. . . . . . . . . . . . 13 class ((𝑓‘𝑘)‘𝑧)
24	19, 16	cfv 5804	. . . . . . . . . . . . 13 class (𝑦‘𝑧)
25		cmin 10145	. . . . . . . . . . . . 13 class −
26	23, 24, 25	co 6549	. . . . . . . . . . . 12 class (((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))
27		cabs 13822	. . . . . . . . . . . 12 class abs
28	26, 27	cfv 5804	. . . . . . . . . . 11 class (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧)))
29		vx	. . . . . . . . . . . 12 setvar 𝑥
30	29	cv 1474	. . . . . . . . . . 11 class 𝑥
31		clt 9953	. . . . . . . . . . 11 class <
32	28, 30, 31	wbr 4583	. . . . . . . . . 10 wff (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥
33	32, 18, 9	wral 2896	. . . . . . . . 9 wff ∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥
34		vj	. . . . . . . . . . 11 setvar 𝑗
35	34	cv 1474	. . . . . . . . . 10 class 𝑗
36	35, 6	cfv 5804	. . . . . . . . 9 class (ℤ≥‘𝑗)
37	33, 20, 36	wral 2896	. . . . . . . 8 wff ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥
38	37, 34, 7	wrex 2897	. . . . . . 7 wff ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥
39		crp 11708	. . . . . . 7 class ℝ+
40	38, 29, 39	wral 2896	. . . . . 6 wff ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥
41	14, 17, 40	w3a 1031	. . . . 5 wff (𝑓:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥)
42		cz 11254	. . . . 5 class ℤ
43	41, 4, 42	wrex 2897	. . . 4 wff ∃𝑛 ∈ ℤ (𝑓:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥)
44	43, 12, 15	copab 4642	. . 3 class {⟨𝑓, 𝑦⟩ ∣ ∃𝑛 ∈ ℤ (𝑓:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥)}
45	2, 3, 44	cmpt 4643	. 2 class (𝑠 ∈ V ↦ {⟨𝑓, 𝑦⟩ ∣ ∃𝑛 ∈ ℤ (𝑓:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥)})
46	1, 45	wceq 1475	1 wff ⇝𝑢 = (𝑠 ∈ V ↦ {⟨𝑓, 𝑦⟩ ∣ ∃𝑛 ∈ ℤ (𝑓:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥)})

This definition is referenced by:  ulmrel  23936  ulmval  23938