Description: The product metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | prdsdsf.y | |
|
prdsdsf.b | |
||
prdsdsf.v | |
||
prdsdsf.e | |
||
prdsdsf.d | |
||
prdsdsf.s | |
||
prdsdsf.i | |
||
prdsdsf.r | |
||
prdsdsf.m | |
||
Assertion | prdsxmetlem | |