Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-metu Unicode version

Definition df-metu 12172
 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 PsMet
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-metu
StepHypRef Expression
1 cmetu 12164 . 2 metUnif
2 vd . . 3
3 cpsmet 12157 . . . . 5 PsMet
43crn 4540 . . . 4 PsMet
54cuni 3736 . . 3 PsMet
62cv 1330 . . . . . . 7
76cdm 4539 . . . . . 6
87cdm 4539 . . . . 5
98, 8cxp 4537 . . . 4
10 va . . . . . 6
11 crp 9448 . . . . . 6
126ccnv 4538 . . . . . . 7
13 cc0 7627 . . . . . . . 8
1410cv 1330 . . . . . . . 8
15 cico 9680 . . . . . . . 8
1613, 14, 15co 5774 . . . . . . 7
1712, 16cima 4542 . . . . . 6
1810, 11, 17cmpt 3989 . . . . 5
1918crn 4540 . . . 4
20 cfg 12162 . . . 4
219, 19, 20co 5774 . . 3
222, 5, 21cmpt 3989 . 2 PsMet
231, 22wceq 1331 1 metUnif PsMet
 Colors of variables: wff set class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator