Description: The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | comet.1 | |
|
comet.2 | |
||
comet.3 | |
||
comet.4 | |
||
comet.5 | |
||
Assertion | comet | |