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

Definition df-ucn 21832
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 = (𝑢 ran UnifOn, 𝑣 ran UnifOn ↦ {𝑓 ∈ (dom 𝑣𝑚 dom 𝑢) ∣ ∀𝑠𝑣𝑟𝑢𝑥 ∈ dom 𝑢𝑦 ∈ dom 𝑢(𝑥𝑟𝑦 → (𝑓𝑥)𝑠(𝑓𝑦))})
Distinct variable group:   𝑣,𝑢,𝑓,𝑠,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-ucn
StepHypRef Expression
1 cucn 21831 . 2 class Cnu
2 vu . . 3 setvar 𝑢
3 vv . . 3 setvar 𝑣
4 cust 21755 . . . . 5 class UnifOn
54crn 5029 . . . 4 class ran UnifOn
65cuni 4366 . . 3 class ran UnifOn
7 vx . . . . . . . . . . 11 setvar 𝑥
87cv 1473 . . . . . . . . . 10 class 𝑥
9 vy . . . . . . . . . . 11 setvar 𝑦
109cv 1473 . . . . . . . . . 10 class 𝑦
11 vr . . . . . . . . . . 11 setvar 𝑟
1211cv 1473 . . . . . . . . . 10 class 𝑟
138, 10, 12wbr 4577 . . . . . . . . 9 wff 𝑥𝑟𝑦
14 vf . . . . . . . . . . . 12 setvar 𝑓
1514cv 1473 . . . . . . . . . . 11 class 𝑓
168, 15cfv 5790 . . . . . . . . . 10 class (𝑓𝑥)
1710, 15cfv 5790 . . . . . . . . . 10 class (𝑓𝑦)
18 vs . . . . . . . . . . 11 setvar 𝑠
1918cv 1473 . . . . . . . . . 10 class 𝑠
2016, 17, 19wbr 4577 . . . . . . . . 9 wff (𝑓𝑥)𝑠(𝑓𝑦)
2113, 20wi 4 . . . . . . . 8 wff (𝑥𝑟𝑦 → (𝑓𝑥)𝑠(𝑓𝑦))
222cv 1473 . . . . . . . . . 10 class 𝑢
2322cuni 4366 . . . . . . . . 9 class 𝑢
2423cdm 5028 . . . . . . . 8 class dom 𝑢
2521, 9, 24wral 2895 . . . . . . 7 wff 𝑦 ∈ dom 𝑢(𝑥𝑟𝑦 → (𝑓𝑥)𝑠(𝑓𝑦))
2625, 7, 24wral 2895 . . . . . 6 wff 𝑥 ∈ dom 𝑢𝑦 ∈ dom 𝑢(𝑥𝑟𝑦 → (𝑓𝑥)𝑠(𝑓𝑦))
2726, 11, 22wrex 2896 . . . . 5 wff 𝑟𝑢𝑥 ∈ dom 𝑢𝑦 ∈ dom 𝑢(𝑥𝑟𝑦 → (𝑓𝑥)𝑠(𝑓𝑦))
283cv 1473 . . . . 5 class 𝑣
2927, 18, 28wral 2895 . . . 4 wff 𝑠𝑣𝑟𝑢𝑥 ∈ dom 𝑢𝑦 ∈ dom 𝑢(𝑥𝑟𝑦 → (𝑓𝑥)𝑠(𝑓𝑦))
3028cuni 4366 . . . . . 6 class 𝑣
3130cdm 5028 . . . . 5 class dom 𝑣
32 cmap 7721 . . . . 5 class 𝑚
3331, 24, 32co 6527 . . . 4 class (dom 𝑣𝑚 dom 𝑢)
3429, 14, 33crab 2899 . . 3 class {𝑓 ∈ (dom 𝑣𝑚 dom 𝑢) ∣ ∀𝑠𝑣𝑟𝑢𝑥 ∈ dom 𝑢𝑦 ∈ dom 𝑢(𝑥𝑟𝑦 → (𝑓𝑥)𝑠(𝑓𝑦))}
352, 3, 6, 6, 34cmpt2 6529 . 2 class (𝑢 ran UnifOn, 𝑣 ran UnifOn ↦ {𝑓 ∈ (dom 𝑣𝑚 dom 𝑢) ∣ ∀𝑠𝑣𝑟𝑢𝑥 ∈ dom 𝑢𝑦 ∈ dom 𝑢(𝑥𝑟𝑦 → (𝑓𝑥)𝑠(𝑓𝑦))})
361, 35wceq 1474 1 wff Cnu = (𝑢 ran UnifOn, 𝑣 ran UnifOn ↦ {𝑓 ∈ (dom 𝑣𝑚 dom 𝑢) ∣ ∀𝑠𝑣𝑟𝑢𝑥 ∈ dom 𝑢𝑦 ∈ dom 𝑢(𝑥𝑟𝑦 → (𝑓𝑥)𝑠(𝑓𝑦))})
Colors of variables: wff setvar class
This definition is referenced by:  ucnval  21833
  Copyright terms: Public domain W3C validator