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

Definition df-metu 17839
Description: Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
Assertion
Ref Expression
df-metu  |- metUnif  =  ( d  e.  U. ran PsMet  |->  ( ( dom  dom  d  X.  dom  dom  d
) filGen ran  ( a  e.  RR+  |->  ( `' d
" ( 0 [,) a ) ) ) ) )
Distinct variable group:    a, d

Detailed syntax breakdown of Definition df-metu
StepHypRef Expression
1 cmetu 17830 . 2  class metUnif
2 vd . . 3  setvar  d
3 cpsmet 17822 . . . . 5  class PsMet
43crn 4862 . . . 4  class  ran PsMet
54cuni 4112 . . 3  class  U. ran PsMet
62cv 1368 . . . . . . 7  class  d
76cdm 4861 . . . . . 6  class  dom  d
87cdm 4861 . . . . 5  class  dom  dom  d
98, 8cxp 4859 . . . 4  class  ( dom 
dom  d  X.  dom  dom  d )
10 va . . . . . 6  setvar  a
11 crp 11012 . . . . . 6  class  RR+
126ccnv 4860 . . . . . . 7  class  `' d
13 cc0 9303 . . . . . . . 8  class  0
1410cv 1368 . . . . . . . 8  class  a
15 cico 11323 . . . . . . . 8  class  [,)
1613, 14, 15co 6112 . . . . . . 7  class  ( 0 [,) a )
1712, 16cima 4864 . . . . . 6  class  ( `' d " ( 0 [,) a ) )
1810, 11, 17cmpt 4371 . . . . 5  class  ( a  e.  RR+  |->  ( `' d " ( 0 [,) a ) ) )
1918crn 4862 . . . 4  class  ran  (
a  e.  RR+  |->  ( `' d " ( 0 [,) a ) ) )
20 cfg 17827 . . . 4  class  filGen
219, 19, 20co 6112 . . 3  class  ( ( dom  dom  d  X.  dom  dom  d ) filGen ran  ( a  e.  RR+  |->  ( `' d " (
0 [,) a ) ) ) )
222, 5, 21cmpt 4371 . 2  class  ( d  e.  U. ran PsMet  |->  ( ( dom  dom  d  X.  dom  dom  d ) filGen ran  ( a  e.  RR+  |->  ( `' d " (
0 [,) a ) ) ) ) )
231, 22wceq 1369 1  wff metUnif  =  ( d  e.  U. ran PsMet  |->  ( ( dom  dom  d  X.  dom  dom  d
) filGen ran  ( a  e.  RR+  |->  ( `' d
" ( 0 [,) a ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  metuval  20147
  Copyright terms: Public domain W3C validator