Description: D is an extended metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rrndsxmet.1 | ||
rrndsxmet.2 | |||
Assertion | rrndsxmet |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rrndsxmet.1 | ||
2 | rrndsxmet.2 | ||
3 | 1 2 | rrndsmet | |
4 | metxmet | ||
5 | 3 4 | syl |