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].Coghetto Roland - Rue de la Brasserie 5, 7100 La Louvière, BelgiumGrzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589–593, 1990.Grzegorz Bancerek. On powers of cardinals. Formalized Mathematics, 3(1):89–93, 1992.Grzegorz Bancerek. The fundamental properties of natural num...