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

Definition df-psmet 16694
 Description: Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)
Assertion
Ref Expression
df-psmet PsMet
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-psmet
StepHypRef Expression
1 cpsmet 16685 . 2 PsMet
2 vx . . 3
3 cvv 2956 . . 3
4 vy . . . . . . . . 9
54cv 1651 . . . . . . . 8
6 vd . . . . . . . . 9
76cv 1651 . . . . . . . 8
85, 5, 7co 6081 . . . . . . 7
9 cc0 8990 . . . . . . 7
108, 9wceq 1652 . . . . . 6
11 vz . . . . . . . . . . 11
1211cv 1651 . . . . . . . . . 10
135, 12, 7co 6081 . . . . . . . . 9
14 vw . . . . . . . . . . . 12
1514cv 1651 . . . . . . . . . . 11
1615, 5, 7co 6081 . . . . . . . . . 10
1715, 12, 7co 6081 . . . . . . . . . 10
18 cxad 10708 . . . . . . . . . 10
1916, 17, 18co 6081 . . . . . . . . 9
20 cle 9121 . . . . . . . . 9
2113, 19, 20wbr 4212 . . . . . . . 8
222cv 1651 . . . . . . . 8
2321, 14, 22wral 2705 . . . . . . 7
2423, 11, 22wral 2705 . . . . . 6
2510, 24wa 359 . . . . 5
2625, 4, 22wral 2705 . . . 4
27 cxr 9119 . . . . 5
2822, 22cxp 4876 . . . . 5
29 cmap 7018 . . . . 5
3027, 28, 29co 6081 . . . 4
3126, 6, 30crab 2709 . . 3
322, 3, 31cmpt 4266 . 2
331, 32wceq 1652 1 PsMet
 Colors of variables: wff set class This definition is referenced by:  ispsmet  18335  metuval  18580  metidval  24285  pstmval  24290
 Copyright terms: Public domain W3C validator