Description: It is safe to only require the triangle inequality when the values are real (so that we can use the standard addition over the reals), but in this case the nonnegativity constraint cannot be deduced and must be provided separately. (Counterexample: D ( x , y ) = if ( x = y , 0 , -oo ) satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isxmetd.0 | |
|
isxmetd.1 | |
||
isxmet2d.2 | |
||
isxmet2d.3 | |
||
isxmet2d.4 | |
||
Assertion | isxmet2d | |