Chebyshev Distance

• Autorzy: Roland Coghetto
• Języki publikacji: EN

Abstrakty

EN

In [21], Marco Riccardi formalized that ℝN-basis n is a basis (in the algebraic sense defined in [26]) of [...] ℰTn ${\cal E}_T^n $ and in [20] he has formalized that [...] ℰTn ${\cal E}_T^n $ is second-countable, we build (in the topological sense defined in [23]) a denumerable base of [...] ℰTn ${\cal E}_T^n $ . 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].

Słowa kluczowe

EN

second-countable; intervals; Chebyshev distance

Kategorie tematyczne

• 03B35: Mechanization of proofs and logical operations
• 54E35: Metric spaces, metrizability

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2016
• Tom: 24
• Numer: 2
• Strony: 121-141

Daty

wydano

2016-06-01

otrzymano

2015-12-31

online

2016-12-08

Twórcy

autor

Roland Coghetto

• Rue de la Brasserie 5, 7100 La Louvière,

Identyfikatory

DOI

10.1515/forma-2016-0010