In [21], Marco Riccardi formalized that ℝN-basis n is a basis (in the algebraic sense defined in [26]) of [...] ℰTn and in [20] he has formalized that [...] ℰTn is second-countable, we build (in the topological sense defined in [23]) a denumerable base of [...] ℰTn . Then we introduce the n-dimensional intervals (interval in n-dimensional Euclidean space, pavé (borné) de ℝn [16], semi-intervalle (borné) de ℝn [22]). We conclude with the definition of Chebyshev distance [11].
@article{bwmeta1.element.doi-10_1515_forma-2016-0010,
author = {Roland Coghetto},
title = {Chebyshev Distance},
journal = {Formalized Mathematics},
volume = {24},
year = {2016},
pages = {121-141},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0010}
}
Roland Coghetto. Chebyshev Distance. Formalized Mathematics, Tome 24 (2016) pp. 121-141. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0010/