Metamath Proof Explorer


Definition df-ucn

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 f is uniformly continuous if, roughly speaking, it is possible to guarantee that ( fx ) and ( fy ) be as close to each other as we please by requiring only that x and y are sufficiently close to each other; unlike ordinary continuity, the maximum distance between ( fx ) and ( fy ) cannot depend on x and y themselves. This formulation is the definition 1 of BourbakiTop1 p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion df-ucn uCn = u ran UnifOn , v ran UnifOn f dom v dom u | s v r u x dom u y dom u x r y f x s f y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cucn class uCn
1 vu setvar u
2 cust class UnifOn
3 2 crn class ran UnifOn
4 3 cuni class ran UnifOn
5 vv setvar v
6 vf setvar f
7 5 cv setvar v
8 7 cuni class v
9 8 cdm class dom v
10 cmap class 𝑚
11 1 cv setvar u
12 11 cuni class u
13 12 cdm class dom u
14 9 13 10 co class dom v dom u
15 vs setvar s
16 vr setvar r
17 vx setvar x
18 vy setvar y
19 17 cv setvar x
20 16 cv setvar r
21 18 cv setvar y
22 19 21 20 wbr wff x r y
23 6 cv setvar f
24 19 23 cfv class f x
25 15 cv setvar s
26 21 23 cfv class f y
27 24 26 25 wbr wff f x s f y
28 22 27 wi wff x r y f x s f y
29 28 18 13 wral wff y dom u x r y f x s f y
30 29 17 13 wral wff x dom u y dom u x r y f x s f y
31 30 16 11 wrex wff r u x dom u y dom u x r y f x s f y
32 31 15 7 wral wff s v r u x dom u y dom u x r y f x s f y
33 32 6 14 crab class f dom v dom u | s v r u x dom u y dom u x r y f x s f y
34 1 5 4 4 33 cmpo class u ran UnifOn , v ran UnifOn f dom v dom u | s v r u x dom u y dom u x r y f x s f y
35 0 34 wceq wff uCn = u ran UnifOn , v ran UnifOn f dom v dom u | s v r u x dom u y dom u x r y f x s f y