Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

Metrics in the Cartesian Product --- Part II


Stanislawa Kanas
Technical University of Rzeszow
Adam Lecko
Technical University of Rzeszow

Summary.

A continuation of [5]. It deals with the method of creation of the distance in the Cartesian product of metric spaces. The distance between two points belonging to Cartesian product of metric spaces has been defined as square root of the sum of squares of distances of appropriate coordinates (or projections) of these points. It is shown that product of metric spaces with such a distance is a metric space. Examples of metric spaces defined in this way are given.

MML Identifier: METRIC_4

The terminology and notation used in this paper have been introduced in the following articles [2] [9] [7] [3] [1] [4] [6] [8]

Contents (PDF format)

  1. Metrics in the Cartesian product of two sets
  2. Metrics in the Cartesian product of three sets

Bibliography

[1] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[3] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.
[4] Stanislawa Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Journal of Formalized Mathematics, 2, 1990.
[5] Stanislawa Kanas and Jan Stankiewicz. Metrics in Cartesian product. Journal of Formalized Mathematics, 2, 1990.
[6] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[7] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[8] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.
[9] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

Received July 8, 1991


[ Download a postscript version, MML identifier index, Mizar home page]