当前位置:文档之家 > The Euclidean Space

The Euclidean Space

FORMALIZED MATHEMATICS

Vol.2, No. 4, September–October1991

Universit´e Catholique de Louvain

The Euclidean Space

Agata Darmochwa l

Warsaw University

Bia l ystok

Summary. The general definitionof Euclidean Space.

MML Identifier:EUCLID .

The papers [14],[6],[9],[8],[12],[1],[5],[10],[3],[13],[4],[15],[16],[7],[11],and [2]provide the notation and terminology for this paper. In the sequel k , n denote natural numbers and r denotes a real number. Let us consider n . The and is definedas functor R n yields a non-empty set of finitesequences of

follows:

(Def.1)R n =n .

In the sequel x will denote a finitesequence of elements of . The function ||from into is definedas follows:

(Def.2)for every r holds ||(r ) =|r |.

Let us consider x . The functor |x |yields a finitesequence of elements of

and is definedas follows:

(Def.3)|x |=||·x .

Let us consider n . T
he functor 0, ... , 0 yields a finitesequence of elements of and is definedby:

Let us consider n . The functor 0, ... , 0 yields a finitesequence of elements of and is definedby:

(Def.4) 0, ... , 0 =n −→0qua a real number . n n

Let us consider n . Then 0, ... , 0 is an element of R n .

In the sequel x , x 1, x 2, y denote elements of R n . One can prove the following proposition

(1)x is an element of n . n

601c 1991Fondation Philippe le Hodey

ISSN 0777–4028

下载Word文档免费下载:

The Euclidean Space下载

(共5页)

TOP相关主题