Description: The product metric is a function into the nonnegative extended reals. In general this means that it is not a metric but rather an *extended* metric (even when all the factors are metrics), but it will be a metric when restricted to regions where it does not take infinite values. (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 | prdsdsf | |