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

Definition df-ulm 23331
 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 there is a such that the functions for are all uniformly within of on the domain . Compare with df-clim 13552. (Contributed by Mario Carneiro, 26-Feb-2015.)
Assertion
Ref Expression
df-ulm
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-ulm
StepHypRef Expression
1 culm 23330 . 2
2 vs . . 3
3 cvv 3080 . . 3
4 vn . . . . . . . . 9
54cv 1436 . . . . . . . 8
6 cuz 11167 . . . . . . . 8
75, 6cfv 5601 . . . . . . 7
8 cc 9545 . . . . . . . 8
92cv 1436 . . . . . . . 8
10 cmap 7484 . . . . . . . 8
118, 9, 10co 6306 . . . . . . 7
12 vf . . . . . . . 8
1312cv 1436 . . . . . . 7
147, 11, 13wf 5597 . . . . . 6
15 vy . . . . . . . 8
1615cv 1436 . . . . . . 7
179, 8, 16wf 5597 . . . . . 6
18 vz . . . . . . . . . . . . . . 15
1918cv 1436 . . . . . . . . . . . . . 14
20 vk . . . . . . . . . . . . . . . 16
2120cv 1436 . . . . . . . . . . . . . . 15
2221, 13cfv 5601 . . . . . . . . . . . . . 14
2319, 22cfv 5601 . . . . . . . . . . . . 13
2419, 16cfv 5601 . . . . . . . . . . . . 13
25 cmin 9868 . . . . . . . . . . . . 13
2623, 24, 25co 6306 . . . . . . . . . . . 12
27 cabs 13298 . . . . . . . . . . . 12
2826, 27cfv 5601 . . . . . . . . . . 11
29 vx . . . . . . . . . . . 12
3029cv 1436 . . . . . . . . . . 11
31 clt 9683 . . . . . . . . . . 11
3228, 30, 31wbr 4423 . . . . . . . . . 10
3332, 18, 9wral 2771 . . . . . . . . 9
34 vj . . . . . . . . . . 11
3534cv 1436 . . . . . . . . . 10
3635, 6cfv 5601 . . . . . . . . 9
3733, 20, 36wral 2771 . . . . . . . 8
3837, 34, 7wrex 2772 . . . . . . 7
39 crp 11310 . . . . . . 7
4038, 29, 39wral 2771 . . . . . 6
4114, 17, 40w3a 982 . . . . 5
42 cz 10945 . . . . 5
4341, 4, 42wrex 2772 . . . 4
4443, 12, 15copab 4481 . . 3
452, 3, 44cmpt 4482 . 2
461, 45wceq 1437 1
 Colors of variables: wff setvar class This definition is referenced by:  ulmrel  23332  ulmval  23334
 Copyright terms: Public domain W3C validator