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 25720
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 15362. (Contributed by Mario Carneiro, 26-Feb-2015.)
Assertion
Ref Expression
df-ulm ⇝𝑒 = (𝑠 ∈ V ↦ {βŸ¨π‘“, π‘¦βŸ© ∣ βˆƒπ‘› ∈ β„€ (𝑓:(β„€β‰₯β€˜π‘›)⟢(β„‚ ↑m 𝑠) ∧ 𝑦:π‘ βŸΆβ„‚ ∧ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘›)βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑠 (absβ€˜(((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§))) < π‘₯)})
Distinct variable group:   𝑓,𝑗,π‘˜,𝑛,𝑠,π‘₯,𝑦,𝑧

Detailed syntax breakdown of Definition df-ulm
StepHypRef Expression
1 culm 25719 . 2 class ⇝𝑒
2 vs . . 3 setvar 𝑠
3 cvv 3443 . . 3 class V
4 vn . . . . . . . . 9 setvar 𝑛
54cv 1540 . . . . . . . 8 class 𝑛
6 cuz 12759 . . . . . . . 8 class β„€β‰₯
75, 6cfv 6493 . . . . . . 7 class (β„€β‰₯β€˜π‘›)
8 cc 11045 . . . . . . . 8 class β„‚
92cv 1540 . . . . . . . 8 class 𝑠
10 cmap 8761 . . . . . . . 8 class ↑m
118, 9, 10co 7353 . . . . . . 7 class (β„‚ ↑m 𝑠)
12 vf . . . . . . . 8 setvar 𝑓
1312cv 1540 . . . . . . 7 class 𝑓
147, 11, 13wf 6489 . . . . . 6 wff 𝑓:(β„€β‰₯β€˜π‘›)⟢(β„‚ ↑m 𝑠)
15 vy . . . . . . . 8 setvar 𝑦
1615cv 1540 . . . . . . 7 class 𝑦
179, 8, 16wf 6489 . . . . . 6 wff 𝑦:π‘ βŸΆβ„‚
18 vz . . . . . . . . . . . . . . 15 setvar 𝑧
1918cv 1540 . . . . . . . . . . . . . 14 class 𝑧
20 vk . . . . . . . . . . . . . . . 16 setvar π‘˜
2120cv 1540 . . . . . . . . . . . . . . 15 class π‘˜
2221, 13cfv 6493 . . . . . . . . . . . . . 14 class (π‘“β€˜π‘˜)
2319, 22cfv 6493 . . . . . . . . . . . . 13 class ((π‘“β€˜π‘˜)β€˜π‘§)
2419, 16cfv 6493 . . . . . . . . . . . . 13 class (π‘¦β€˜π‘§)
25 cmin 11381 . . . . . . . . . . . . 13 class βˆ’
2623, 24, 25co 7353 . . . . . . . . . . . 12 class (((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§))
27 cabs 15111 . . . . . . . . . . . 12 class abs
2826, 27cfv 6493 . . . . . . . . . . 11 class (absβ€˜(((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§)))
29 vx . . . . . . . . . . . 12 setvar π‘₯
3029cv 1540 . . . . . . . . . . 11 class π‘₯
31 clt 11185 . . . . . . . . . . 11 class <
3228, 30, 31wbr 5103 . . . . . . . . . 10 wff (absβ€˜(((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§))) < π‘₯
3332, 18, 9wral 3062 . . . . . . . . 9 wff βˆ€π‘§ ∈ 𝑠 (absβ€˜(((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§))) < π‘₯
34 vj . . . . . . . . . . 11 setvar 𝑗
3534cv 1540 . . . . . . . . . 10 class 𝑗
3635, 6cfv 6493 . . . . . . . . 9 class (β„€β‰₯β€˜π‘—)
3733, 20, 36wral 3062 . . . . . . . 8 wff βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑠 (absβ€˜(((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§))) < π‘₯
3837, 34, 7wrex 3071 . . . . . . 7 wff βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘›)βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑠 (absβ€˜(((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§))) < π‘₯
39 crp 12907 . . . . . . 7 class ℝ+
4038, 29, 39wral 3062 . . . . . 6 wff βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘›)βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑠 (absβ€˜(((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§))) < π‘₯
4114, 17, 40w3a 1087 . . . . 5 wff (𝑓:(β„€β‰₯β€˜π‘›)⟢(β„‚ ↑m 𝑠) ∧ 𝑦:π‘ βŸΆβ„‚ ∧ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘›)βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑠 (absβ€˜(((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§))) < π‘₯)
42 cz 12495 . . . . 5 class β„€
4341, 4, 42wrex 3071 . . . 4 wff βˆƒπ‘› ∈ β„€ (𝑓:(β„€β‰₯β€˜π‘›)⟢(β„‚ ↑m 𝑠) ∧ 𝑦:π‘ βŸΆβ„‚ ∧ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘›)βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑠 (absβ€˜(((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§))) < π‘₯)
4443, 12, 15copab 5165 . . 3 class {βŸ¨π‘“, π‘¦βŸ© ∣ βˆƒπ‘› ∈ β„€ (𝑓:(β„€β‰₯β€˜π‘›)⟢(β„‚ ↑m 𝑠) ∧ 𝑦:π‘ βŸΆβ„‚ ∧ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘›)βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑠 (absβ€˜(((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§))) < π‘₯)}
452, 3, 44cmpt 5186 . 2 class (𝑠 ∈ V ↦ {βŸ¨π‘“, π‘¦βŸ© ∣ βˆƒπ‘› ∈ β„€ (𝑓:(β„€β‰₯β€˜π‘›)⟢(β„‚ ↑m 𝑠) ∧ 𝑦:π‘ βŸΆβ„‚ ∧ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘›)βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑠 (absβ€˜(((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§))) < π‘₯)})
461, 45wceq 1541 1 wff ⇝𝑒 = (𝑠 ∈ V ↦ {βŸ¨π‘“, π‘¦βŸ© ∣ βˆƒπ‘› ∈ β„€ (𝑓:(β„€β‰₯β€˜π‘›)⟢(β„‚ ↑m 𝑠) ∧ 𝑦:π‘ βŸΆβ„‚ ∧ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘›)βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑠 (absβ€˜(((π‘“β€˜π‘˜)β€˜π‘§) βˆ’ (π‘¦β€˜π‘§))) < π‘₯)})
Colors of variables: wff setvar class
This definition is referenced by:  ulmrel  25721  ulmval  25723
  Copyright terms: Public domain W3C validator