MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ulm Structured version   Visualization version   GIF version

Definition df-ulm 23852
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 14013. (Contributed by Mario Carneiro, 26-Feb-2015.)
Assertion
Ref Expression
df-ulm 𝑢 = (𝑠 ∈ V ↦ {⟨𝑓, 𝑦⟩ ∣ ∃𝑛 ∈ ℤ (𝑓:(ℤ𝑛)⟶(ℂ ↑𝑚 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ (ℤ𝑛)∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑠 (abs‘(((𝑓𝑘)‘𝑧) − (𝑦𝑧))) < 𝑥)})
Distinct variable group:   𝑓,𝑗,𝑘,𝑛,𝑠,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ulm
StepHypRef Expression
1 culm 23851 . 2 class 𝑢
2 vs . . 3 setvar 𝑠
3 cvv 3172 . . 3 class V
4 vn . . . . . . . . 9 setvar 𝑛
54cv 1473 . . . . . . . 8 class 𝑛
6 cuz 11519 . . . . . . . 8 class
75, 6cfv 5790 . . . . . . 7 class (ℤ𝑛)
8 cc 9790 . . . . . . . 8 class
92cv 1473 . . . . . . . 8 class 𝑠
10 cmap 7721 . . . . . . . 8 class 𝑚
118, 9, 10co 6527 . . . . . . 7 class (ℂ ↑𝑚 𝑠)
12 vf . . . . . . . 8 setvar 𝑓
1312cv 1473 . . . . . . 7 class 𝑓
147, 11, 13wf 5786 . . . . . 6 wff 𝑓:(ℤ𝑛)⟶(ℂ ↑𝑚 𝑠)
15 vy . . . . . . . 8 setvar 𝑦
1615cv 1473 . . . . . . 7 class 𝑦
179, 8, 16wf 5786 . . . . . 6 wff 𝑦:𝑠⟶ℂ
18 vz . . . . . . . . . . . . . . 15 setvar 𝑧
1918cv 1473 . . . . . . . . . . . . . 14 class 𝑧
20 vk . . . . . . . . . . . . . . . 16 setvar 𝑘
2120cv 1473 . . . . . . . . . . . . . . 15 class 𝑘
2221, 13cfv 5790 . . . . . . . . . . . . . 14 class (𝑓𝑘)
2319, 22cfv 5790 . . . . . . . . . . . . 13 class ((𝑓𝑘)‘𝑧)
2419, 16cfv 5790 . . . . . . . . . . . . 13 class (𝑦𝑧)
25 cmin 10117 . . . . . . . . . . . . 13 class
2623, 24, 25co 6527 . . . . . . . . . . . 12 class (((𝑓𝑘)‘𝑧) − (𝑦𝑧))
27 cabs 13768 . . . . . . . . . . . 12 class abs
2826, 27cfv 5790 . . . . . . . . . . 11 class (abs‘(((𝑓𝑘)‘𝑧) − (𝑦𝑧)))
29 vx . . . . . . . . . . . 12 setvar 𝑥
3029cv 1473 . . . . . . . . . . 11 class 𝑥
31 clt 9930 . . . . . . . . . . 11 class <
3228, 30, 31wbr 4577 . . . . . . . . . 10 wff (abs‘(((𝑓𝑘)‘𝑧) − (𝑦𝑧))) < 𝑥
3332, 18, 9wral 2895 . . . . . . . . 9 wff 𝑧𝑠 (abs‘(((𝑓𝑘)‘𝑧) − (𝑦𝑧))) < 𝑥
34 vj . . . . . . . . . . 11 setvar 𝑗
3534cv 1473 . . . . . . . . . 10 class 𝑗
3635, 6cfv 5790 . . . . . . . . 9 class (ℤ𝑗)
3733, 20, 36wral 2895 . . . . . . . 8 wff 𝑘 ∈ (ℤ𝑗)∀𝑧𝑠 (abs‘(((𝑓𝑘)‘𝑧) − (𝑦𝑧))) < 𝑥
3837, 34, 7wrex 2896 . . . . . . 7 wff 𝑗 ∈ (ℤ𝑛)∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑠 (abs‘(((𝑓𝑘)‘𝑧) − (𝑦𝑧))) < 𝑥
39 crp 11664 . . . . . . 7 class +
4038, 29, 39wral 2895 . . . . . 6 wff 𝑥 ∈ ℝ+𝑗 ∈ (ℤ𝑛)∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑠 (abs‘(((𝑓𝑘)‘𝑧) − (𝑦𝑧))) < 𝑥
4114, 17, 40w3a 1030 . . . . 5 wff (𝑓:(ℤ𝑛)⟶(ℂ ↑𝑚 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ (ℤ𝑛)∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑠 (abs‘(((𝑓𝑘)‘𝑧) − (𝑦𝑧))) < 𝑥)
42 cz 11210 . . . . 5 class
4341, 4, 42wrex 2896 . . . 4 wff 𝑛 ∈ ℤ (𝑓:(ℤ𝑛)⟶(ℂ ↑𝑚 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ (ℤ𝑛)∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑠 (abs‘(((𝑓𝑘)‘𝑧) − (𝑦𝑧))) < 𝑥)
4443, 12, 15copab 4636 . . 3 class {⟨𝑓, 𝑦⟩ ∣ ∃𝑛 ∈ ℤ (𝑓:(ℤ𝑛)⟶(ℂ ↑𝑚 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ (ℤ𝑛)∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑠 (abs‘(((𝑓𝑘)‘𝑧) − (𝑦𝑧))) < 𝑥)}
452, 3, 44cmpt 4637 . 2 class (𝑠 ∈ V ↦ {⟨𝑓, 𝑦⟩ ∣ ∃𝑛 ∈ ℤ (𝑓:(ℤ𝑛)⟶(ℂ ↑𝑚 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ (ℤ𝑛)∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑠 (abs‘(((𝑓𝑘)‘𝑧) − (𝑦𝑧))) < 𝑥)})
461, 45wceq 1474 1 wff 𝑢 = (𝑠 ∈ V ↦ {⟨𝑓, 𝑦⟩ ∣ ∃𝑛 ∈ ℤ (𝑓:(ℤ𝑛)⟶(ℂ ↑𝑚 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ (ℤ𝑛)∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑠 (abs‘(((𝑓𝑘)‘𝑧) − (𝑦𝑧))) < 𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  ulmrel  23853  ulmval  23855
  Copyright terms: Public domain W3C validator