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

Definition df-ucn 20757
 Description: Define a function on two uniform structures which value is the set of uniformly continuous functions from the first uniform structure to the second. A function is uniformly continuous if, roughly speaking, it is possible to guarantee that and be as close to each other as we please by requiring only that and are sufficiently close to each other; unlike ordinary continuity, the maximum distance between and cannot depend on and themselves. This formulation is the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
Assertion
Ref Expression
df-ucn Cnu UnifOn UnifOn
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-ucn
StepHypRef Expression
1 cucn 20756 . 2 Cnu
2 vu . . 3
3 vv . . 3
4 cust 20680 . . . . 5 UnifOn
54crn 4990 . . . 4 UnifOn
65cuni 4234 . . 3 UnifOn
7 vx . . . . . . . . . . 11
87cv 1382 . . . . . . . . . 10
9 vy . . . . . . . . . . 11
109cv 1382 . . . . . . . . . 10
11 vr . . . . . . . . . . 11
1211cv 1382 . . . . . . . . . 10
138, 10, 12wbr 4437 . . . . . . . . 9
14 vf . . . . . . . . . . . 12
1514cv 1382 . . . . . . . . . . 11
168, 15cfv 5578 . . . . . . . . . 10
1710, 15cfv 5578 . . . . . . . . . 10
18 vs . . . . . . . . . . 11
1918cv 1382 . . . . . . . . . 10
2016, 17, 19wbr 4437 . . . . . . . . 9
2113, 20wi 4 . . . . . . . 8
222cv 1382 . . . . . . . . . 10
2322cuni 4234 . . . . . . . . 9
2423cdm 4989 . . . . . . . 8
2521, 9, 24wral 2793 . . . . . . 7
2625, 7, 24wral 2793 . . . . . 6
2726, 11, 22wrex 2794 . . . . 5
283cv 1382 . . . . 5
2927, 18, 28wral 2793 . . . 4
3028cuni 4234 . . . . . 6
3130cdm 4989 . . . . 5
32 cmap 7422 . . . . 5
3331, 24, 32co 6281 . . . 4
3429, 14, 33crab 2797 . . 3
352, 3, 6, 6, 34cmpt2 6283 . 2 UnifOn UnifOn
361, 35wceq 1383 1 Cnu UnifOn UnifOn
 Colors of variables: wff setvar class This definition is referenced by:  ucnval  20758
 Copyright terms: Public domain W3C validator