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

Definition df-ulm 20298
 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 12287. (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 20297 . 2
2 vs . . 3
3 cvv 2958 . . 3
4 vn . . . . . . . . 9
54cv 1652 . . . . . . . 8
6 cuz 10493 . . . . . . . 8
75, 6cfv 5457 . . . . . . 7
8 cc 8993 . . . . . . . 8
92cv 1652 . . . . . . . 8
10 cmap 7021 . . . . . . . 8
118, 9, 10co 6084 . . . . . . 7
12 vf . . . . . . . 8
1312cv 1652 . . . . . . 7
147, 11, 13wf 5453 . . . . . 6
15 vy . . . . . . . 8
1615cv 1652 . . . . . . 7
179, 8, 16wf 5453 . . . . . 6
18 vz . . . . . . . . . . . . . . 15
1918cv 1652 . . . . . . . . . . . . . 14
20 vk . . . . . . . . . . . . . . . 16
2120cv 1652 . . . . . . . . . . . . . . 15
2221, 13cfv 5457 . . . . . . . . . . . . . 14
2319, 22cfv 5457 . . . . . . . . . . . . 13
2419, 16cfv 5457 . . . . . . . . . . . . 13
25 cmin 9296 . . . . . . . . . . . . 13
2623, 24, 25co 6084 . . . . . . . . . . . 12
27 cabs 12044 . . . . . . . . . . . 12
2826, 27cfv 5457 . . . . . . . . . . 11
29 vx . . . . . . . . . . . 12
3029cv 1652 . . . . . . . . . . 11
31 clt 9125 . . . . . . . . . . 11
3228, 30, 31wbr 4215 . . . . . . . . . 10
3332, 18, 9wral 2707 . . . . . . . . 9
34 vj . . . . . . . . . . 11
3534cv 1652 . . . . . . . . . 10
3635, 6cfv 5457 . . . . . . . . 9
3733, 20, 36wral 2707 . . . . . . . 8
3837, 34, 7wrex 2708 . . . . . . 7
39 crp 10617 . . . . . . 7
4038, 29, 39wral 2707 . . . . . 6
4114, 17, 40w3a 937 . . . . 5
42 cz 10287 . . . . 5
4341, 4, 42wrex 2708 . . . 4
4443, 12, 15copab 4268 . . 3
452, 3, 44cmpt 4269 . 2
461, 45wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  ulmrel  20299  ulmval  20301
 Copyright terms: Public domain W3C validator