FORMALIZED MATHEMATICS Volume 11, Number 2, 2003 University of Białystok

Improvement of Radix-2^{k} Signed-Digit Number for High Speed Circuit

Masaaki Niimura Shinshu University Nagano

Yasushi Fuwa Shinshu University Nagano

Summary. In this article, a new radix-2^{k} signed-digit number (Radix-2^{k} sub signed-digit number) is defined and its properties for hardware realization are discussed.

Until now, high speed calculation method with Radix-2^{k} signed-digit numbers is proposed, but this method used “Compares With 2” to calculate carry. “Compares with 2” is a very simple method, but it needs very complicated hardware especially when the value of k becomes large. In this article, we propose a subset of Radix-2^{k} signed-digit, named Radix-2^{k} sub signed-digit numbers. Radix-2^{k} sub signed-digit was designed so that the carry calculation use “bit compare” to hardware-realization simplifies more.

In the first section of this article, we defined the concept of Radix-2^{k} sub signed-digit numbers and proved some of their properties. In the second section, we defined the new carry calculation method in consideration of hardwarerealization, and proved some of their properties. In the third section, we provide some functions for generating Radix-2^{k} sub signed-digit numbers from Radix-2^{k} signed-digit numbers. In the last section, we defined some functions for generation natural numbers from Radix-2^{k} sub signed-digit, and we clarified its correctness.

MML Identifier: RADIX 3.

The articles [11], [14], [8], [12], [1], [4], [3], [13], [10], [7], [2], [9], [5], and [6] provide the notation and terminology for this paper.

1. Definition for Radix-2^{k} Sub Signed-Digit Number

We adopt the following convention: i, n, m, k, x are natural numbers and i_{1}, i_{2} are integers.

Next we state the proposition (1) ((Radixk)_{ℕ}^{n}) · Radixk = (Radixk)_{ℕ}^{n+1}. Let us consider k. The functor k −SD Sub S is defined as follows:

(Def. 1) k −SD Sub S = {e; e ranges over elements of ℤ: e − Radix(k − ′1) ∧

e Radix(k − ′1) − 1}. Let us consider k. The functor k −SD Sub is defined by:

(Def. 2) k −SD Sub = {e; e ranges over elements of ℤ: e − Radix(k − ′1) − 1 ∧

e Radix(k − ′1)}. The following propositions are true:

(2) If i_{1} ∈ k −SD Sub , then − Radix(k − ′1) − 1 i_{1} and i_{1} Radix(k − ′1).

(3) For every natural number k holds k −SD Sub S ⊆ k −SD Sub .

(4) k −SD Sub S ⊆ (k + 1) −SD Sub S .

(5) For every natural number k such that 2 k holds k −SD Sub ⊆ k −SD .

(6) 0 ∈ 0 −SD Sub S .

(7) 0 ∈ k −SD Sub S .

(8) 0 ∈ k −SD Sub .

(9) For every set e such that e ∈ k −SD Sub holds e is an integer.

(10) k −SD Sub ⊆ ℤ.

(11) k −SD Sub S ⊆ ℤ.

Let us consider k. One can verify that k −SD Sub S is non empty. Let us consider k. Note that k −SD Sub is non empty. Let us consider k. Then k −SD Sub S is a non empty subset of ℤ. Let us consider k. Then k −SD Sub is a non empty subset of ℤ. In the sequel a denotes a n-tuple of k −SD and a_{1} denotes a n-tuple of

k −SD Sub .

One can prove the following proposition

(12) If i ∈ Segn, then a_{1}(i) is an element of k −SD Sub .

2. Definition for New Carry Calculation Method

Let x be an integer and let k be a natural number. The functor SDSubAddCarry(x, k) yields an integer and is defined as follows:

(Def. 3) SDSubAddCarry(x, k) = \{ \begin{matrix}1, if Radix(k − ′1) x, \\ − 1, if x < − Radix(k − ′1), \\ 0, otherwise. \end{matrix}

Let x be an integer and let k be a natural number. The functor SDSubAddData(x, k) yields an integer and is defined as follows:

(Def. 4) SDSubAddData(x, k) = x − Radixk · SDSubAddCarry(x, k). One can prove the following propositions:

improvement of radix-2^{k} signed-digit … 135

(13) For every integer x and for every natural number k such that 2 k holds − 1 SDSubAddCarry(x, k) and SDSubAddCarry(x, k) 1.

(14) If 2 k and i_{1} ∈ k −SD , then SDSubAddData(i_{1}, k) − Radix(k − ′1) and SDSubAddData(i_{1}, k) Radix(k − ′1) − 1.

(15) For every integer x and for every natural number k such that 2 k holds SDSubAddCarry(x, k) ∈ k −SD Sub S .

(16) If 2 k and i_{1} ∈ k −SD and i_{2} ∈ k −SD , then SDSubAddData(i_{1}, k) + SDSubAddCarry(i_{2}, k) ∈ k −SD Sub .

(17) If 2 k, then SDSubAddCarry(0, k) = 0.

3. Definition for Translation from Radix-2^{k} Signed-Digit Number

Let i, k, n be natural numbers and let x be a n-tuple of k −SD Sub . The functor DigA SDSub(x, i) yields an integer and is defined as follows:

(Def. 5)(i) DigA SDSub(x, i) = x(i) if i ∈ Segn, (ii) DigA SDSub(x, i) = 0 if i = 0. Let i, k, n be natural numbers and let x be a n-tuple of k −SD . The functor

SD2SDSubDigit(x, i, k) yields an integer and is defined by:

(Def. 6) SD2SDSubDigit(x, i, k) = \begin{cases}(i)SDSubAddData(DigA(x, i), k)+ \\ SDSubAddCarry(DigA(x, i − ′1), k), \\ if i ∈ Segn, \\ (ii)SDSubAddCarry(DigA(x, i − ′1), k), \\ if i = n + 1, \\ 0, otherwise. \end{cases}

We now state the proposition

(18) If 2 k and i ∈ Seg(n + 1), then SD2SDSubDigit(a, i, k) is an element

of k −SD Sub . Let i, k, n be natural numbers and let x be a n-tuple of k −SD . Let us

assume that 2 k and i ∈ Seg(n + 1). The functor SD2SDSubDigitS(x, i, k) yielding an element of k −SD Sub is defined by:

(Def. 7) SD2SDSubDigitS(x, i, k) = SD2SDSubDigit(x, i, k).

Let n, k be natural numbers and let x be a n-tuple of k −SD . The functor SD2SDSubx yielding a n + 1-tuple of k −SD Sub is defined by:

(Def. 8) For every natural number i such that i ∈ Seg(n + 1) holds

DigA SDSub(SD2SDSubx, i) = SD2SDSubDigitS(x, i, k). Next we state two propositions:

(19) If i ∈ Segn, then DigA SDSub(a_{1}, i) is an element of k −SD Sub .

(20) If 2 k and i_{1} ∈ k −SD and i_{2} ∈ k −SD Sub , then SDSubAddData(i_{1} + i_{2}, k) ∈ k −SD Sub S .

136 masaaki niimura and yasushi fuwa

4. Definiton for Translation from Radix-2^{k} Sub Signed-Digit Number to INT

Let i, k, n be natural numbers and let x be a n-tuple of k −SD Sub . The functor DigB SDSub(x, i) yielding an element of ℤ is defined by:

(Def. 9) DigB SDSub(x, i) = DigA SDSub(x, i). Let i, k, n be natural numbers and let x be a n-tuple of k −SD Sub . The

functor SDSub2INTDigit(x, i, k) yielding an element of ℤ is defined as follows: (Def. 10) SDSub2INTDigit(x, i, k) = ((Radixk)_{ℕ}^{i− ′1}) · DigB SDSub(x, i).

Let n, k be natural numbers and let x be a n-tuple of k −SD Sub . The functor SDSub2INTx yields a n-tuple of ℤ and is defined as follows:

(Def. 11) For every natural number i such that i ∈ Segn holds (SDSub2INTx)_{i} = SDSub2INTDigit(x, i, k).

Let n, k be natural numbers and let x be a n-tuple of k −SD Sub . The functor SDSub2IntOutx yields an integer and is defined as follows:

(Def. 12) SDSub2IntOutx = ∑ SDSub2INTx.

Next we state two propositions:

(21) For every i such that i ∈ Segn holds if 2 k, then DigA SDSub(SD2SDSubDecSD(m, n + 1, k), i) = DigA SDSub(SD2SDSubDecSD(m mod (Radixk)_{ℕ}^{n}, n, k), i).

(22) For every n such that n 1 and for all k, x such that k 2 and x is represented by n, k holds x = SDSub2IntOutSD2SDSubDecSD(x, n, k).

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek. Joining of decorated trees. Formalized Mathematics, 4(1):77–82, 1993.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[4] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[5] Marek Chmur. The lattice of natural numbers and the sublattice of it. The set of prime numbers. Formalized Mathematics, 2(4):453–459, 1991.

[6] Yoshinori Fujisawa and Yasushi Fuwa. Definitions of radix-2^{k} signed-digit number and its adder algorithm. Formalized Mathematics, 9(1):71–75, 2001.

[7] Yoshinori Fujisawa, Yasushi Fuwa, and Hidetaka Shimizu. Euler’s Theorem and small Fermat’s Theorem. Formalized Mathematics, 7(1):123–126, 1998.

[8] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[9] Andrzej Kondracki. The Chinese Remainder Theorem. Formalized Mathematics, 6(4):573–577, 1997.

[10] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Formalized Mathematics, 4(1):83–86, 1993.

[11] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[12] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990.

improvement of radix-2^{k} signed-digit … 137

[13] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579, 1990.

[14] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

Received January 3, 2003

High Speed Adder Algorithm with Radix-2^{k} Sub Signed-Digit Number

Masaaki Niimura Shinshu University Nagano

Yasushi Fuwa Shinshu University Nagano

Summary. In this article, a new adder algorithm using Radix-2^{k} sub signed-digit numbers is defined and properties for the hardware-realization is discussed.

Until now, we proposed Radix-2^{k} sub signed-digit numbers in consideration of the hardware realization. In this article, we proposed High Speed Adder Algorithm using this Radix-2^{k} sub signed-digit numbers. This method has two ways to speed up at hardware-realization. One is ’bit compare’ at carry calculation, it is proposed in another article. Other is carry calculation between two numbers. We proposed that n digits Radix-2^{k} signed-digit numbers is expressed in n + 1 digits Radix-2^{k} sub signed-digit numbers, and addition result of two n + 1 digits Radix-2^{k} sub signed-digit numbers is expressed in n + 1 digits. In this way, carry operation between two Radix-2^{k} sub signed-digit numbers can be processed at n + 1 digit adder circuit and additional circuit to operate carry is not needed.

In the first section of this article, we prepared some useful theorems for operation of Radix-2^{k} numbers. In the second section, we proved some properties about carry on Radix-2^{k} sub signed-digit numbers. In the last section, we defined the new addition operation using Radix-2^{k} sub signed-digit numbers, and we clarified its correctness.

MML Identifier: RADIX 4.

The terminology and notation used here are introduced in the following articles: [11], [13], [12], [1], [4], [3], [10], [7], [2], [8], [5], [6], and [9].

1. Preliminaries

In this paper i, n, m, k, x, y are natural numbers. The following proposition is true (1) For every natural number k such that 2 k holds 2 < Radixk.

2. Carry Operation at n + 1 Digits Radix-2^{k} Sub Signed-Digit Number

The following propositions are true:

(2) For all integers x, y and for every natural number k such that 3 k holds SDSubAddCarry(SDSubAddCarry(x, k) + SDSubAddCarry(y, k), k) = 0.

(3) If 2 k, then DigA SDSub(SD2SDSubDecSD(m, n, k), n + 1) = SDSubAddCarry(DigA(DecSD(m, n, k), n), k).

(4) If 2 k and m is represented by 1, k, then DigA SDSub(SD2SDSubDecSD(m, 1, k), 1+1) = SDSubAddCarry(m, k).

(5) Let k, x, n be natural numbers. Suppose n 1 and k 3 and x is represented by n + 1, k. Then DigA SDSub(SD2SDSubDecSD(x mod (Radixk)_{ℕ}^{n}, n, k), n + 1) = SDSubAddCarry(DigA(DecSD(x, n, k), n), k).

(6) If 2 k and m is represented by 1, k, then DigA SDSub(SD2SDSubDecSD(m, 1, k), 1) = m−SDSubAddCarry(m, k)· Radixk.

(7) Let k, x, n be natural numbers. Suppose n 1 and k 2 and x is represented by n + 1, k. Then ((Radixk)_{ℕ}^{n}) · DigA SDSub(SD2SDSubDecSD(x, n + 1, k), n + 1) = (((Radixk)_{ℕ}^{n}) · DigA(DecSD(x, n + 1, k), n + 1) − ((Radixk)_{ℕ}^{n+1}) · SDSubAddCarry(DigA (DecSD(x, n+1, k), n+1), k))+((Radixk)_{ℕ}^{n})·SDSubAddCarry(DigA(DecSD (x, n + 1, k), n), k).

3. Definition for Adder Operation on Radix-2^{k} Sub Signed-Digit Number

Let i, n, k be natural numbers, let x be a n-tuple of k −SD Sub , and let y be a n-tuple of k −SD Sub . Let us assume that i ∈ Segn and k 2. The functor SDSubAddDigit(x, y, i, k) yields an element of k −SD Sub and is defined as follows:

(Def. 1) SDSubAddDigit(x, y, i, k) = SDSubAddData(DigA SDSub(x, i)+ DigA SDSub(y, i), k) + SDSubAddCarry(DigA SDSub(x, i − ′1)+ DigA SDSub(y, i − ′1), k).

Let n, k be natural numbers and let x, y be n-tuples of k −SD Sub . The functor x′+′y yields a n-tuple of k −SD Sub and is defined by:

(Def. 2) For every i such that i ∈ Segn holds DigA SDSub(x′ +′ y, i) = SDSubAddDigit(x, y, i, k).

high speed adder algorithm with radix-2^{k} … 141

Next we state two propositions:

(8) For every i such that i ∈ Segn holds if 2 k, then SDSubAddDigit(SD2SDSubDecSD(x, n + 1, k), SD2SDSubDecSD(y, n + 1, k), i, k) = SDSubAddDigit(SD2SDSubDecSD(x mod (Radixk)_{ℕ}^{n}, n, k), SD2SDSubDecSD(y mod (Radixk)_{ℕ}^{n}, n, k), i, k).

(9) Let given n. Suppose n 1. Let given k, x, y. Suppose k 3 and x is represented by n, k and y is represented by n, k. Then x + y = SDSub2IntOutSD2SDSubDecSD(x, n, k)′+′SD2SDSubDecSD(y, n, k).

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek. Joining of decorated trees. Formalized Mathematics, 4(1):77–82, 1993.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[4] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[5] Marek Chmur. The lattice of natural numbers and the sublattice of it. The set of prime numbers. Formalized Mathematics, 2(4):453–459, 1991.

[6] Yoshinori Fujisawa and Yasushi Fuwa. Definitions of radix-2^{k} signed-digit number and its adder algorithm. Formalized Mathematics, 9(1):71–75, 2001.

[7] Yoshinori Fujisawa, Yasushi Fuwa, and Hidetaka Shimizu. Euler’s Theorem and small Fermat’s Theorem. Formalized Mathematics, 7(1):123–126, 1998.

[8] Andrzej Kondracki. The Chinese Remainder Theorem. Formalized Mathematics, 6(4):573–577, 1997.

[9] Masaaki Niimura and Yasushi Fuwa. Improvement of radix-2^{k} signed-digit number for high speed circuit. Formalized Mathematics, 11(2):133–137, 2003.

[10] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Formalized Mathematics, 4(1):83–86, 1993.

[11] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[12] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990.

[13] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

The Underlying Principle of Dijkstra’s Shortest Path Algorithm

Jing-Chao Chen Donghua University Shanghai Yatsuka Nakamura Shinshu University Nagano

Summary. A path from a source vertex v to a target vertex u is said to be a shortest path if its total cost is minimum among all v-to-u paths. Dijkstra’s algorithm is a classic shortest path algorithm, which is described in many textbooks. To justify its correctness (whose rigorous proof will be given in the next article), it is necessary to clarify its underlying principle. For this purpose, the article justifies the following basic facts, which are the core of Dijkstra’s algorithm.

• A graph is given, its vertex set is denoted by V. Assume U is the subset of V, and if a path p from s to t is the shortest among the set of paths, each of which passes through only the vertices in U, except the source and sink, and its source and sink is s and in V, respectively, then p is a shortest path from s to t in the graph, and for any subgraph which contains at least U, it is also the shortest.

• Let p(s, x, U) denote the shortest path from s to x in a subgraph whose the vertex set is the union of {s, x} and U, and cost (p) denote the cost of path p(s, x, U), cost(x, y) the cost of the edge from x to y. Give p(s, x, U), q(s, y, U) and r(s, y, U ∪{x}). If cost(p) = min{cost(w) : w(s, t, U)∧t ∈ V }, then we have

cost(r) = min(cost(p) + cost(x, y), cost(q)).

This is the well-known triangle comparison of Dijkstra’s algorithm.

MML Identifier: GRAPH 5.

The articles [14], [16], [13], [17], [5], [3], [4], [15], [1], [8], [9], [2], [10], [6], [12], [7], and [11] provide the terminology and notation for this paper.

1. Preliminaries

We follow the rules: n, m, i, j, k denote natural numbers, x, y, e, X, V, U denote sets, and W, f, g denote functions.

Let f be a finite function. Observe that rngf is finite. One can prove the following two propositions:

(1) For every finite function f holds cardrngf carddomf.

(2) If rngf ⊆ rngg and x ∈ domf, then there exists y such that y ∈ domg and f(x) = g(y).

The scheme LambdaAB deals with sets A, B and a unary functor F yielding a set, and states that:

There exists a function f such that domf = A and for every element x of B such that x ∈ A holds f(x) = F(x)

for all values of the parameters.

The following propositions are true:

(3) Let D be a finite set, n be a natural number, and X be a set. If X = {x; x ranges over elements of D^{∗}: 1 lenx ∧ lenx n}, then X is finite.

(4) Let D be a finite set, n be a natural number, and X be a set. If X = {x; x ranges over elements of D^{∗}: lenx n}, then X is finite.

(5) For every finite set D holds cardD ≠ 0 iff D ≠ ∅.

(6) Let D be a finite set and k be a natural number. Suppose cardD = k+1. Then there exists an element x of D and there exists a subset C of D such that D = C ∪ {x} and cardC = k.

(7) For every finite set D such that cardD = 1 there exists an element x of D such that D = {x}.

The scheme MinValue deals with a non empty finite set A and a unary functor F yielding a real number, and states that:

There exists an element x of A such that for every element y of A holds F(x) F(y)

for all values of the parameters.

Let D be a set and let X be a non empty subset of D^{∗}. We see that the element of X is a finite sequence of elements of D.

2. Additional Properties of Finite Sequences

In the sequel p, q are finite sequences. One can prove the following propositions:

(8) p ≠ ∅ iff lenp 1.

(9) For all n, m such that 1 n and n < m and m lenp holds p(n) ≠ p(m) iff p is one-to-one.

(10) For all n, m such that 1 n and n < m and m lenp holds p(n) ≠ p(m)

iff cardrngp = lenp. In the sequel G denotes a graph and p_{1}, q_{1} denote finite sequences of elements

of the edges of G.

Next we state two propositions:

(11) If i ∈ domp_{1}, then (the source of G)(p_{1}(i)) ∈ the vertices of G and (the target of G)(p_{1}(i)) ∈ the vertices of G.

(12) If q ^{⌢} ⟨x⟩ is one-to-one and rng(q ^{⌢} ⟨x⟩) ⊆ rngp, then there exist finite sequences p_{2}, p_{3} such that p = p_{2} ^{⌢} ⟨x⟩^{⌢} p_{3} and rngq ⊆ rng(p_{2} ^{⌢} p_{3}).

3. Additional Properties of Chains and Oriented Paths

One can prove the following three propositions:

(13) If p^{⌢} q is a chain of G, then p is a chain of G and q is a chain of G.

(14) If p^{⌢} q is an oriented chain of G, then p is an oriented chain of G and q is an oriented chain of G.

(15) Let p, q be oriented chains of G. Suppose (the target of G)(p(lenp)) = (the source of G)(q(1)). Then p^{⌢} q is an oriented chain of G.

4. Additional Properties of Acyclic Oriented Paths

The following propositions are true:

(16) ∅ is a Simple oriented chain of G.

(17) Suppose p^{⌢}q is a Simple oriented chain of G. Then p is a Simple oriented chain of G and q is a Simple oriented chain of G.

(18) If lenp_{1} = 1, then p_{1} is a Simple oriented chain of G.

(19) Let p be a Simple oriented chain of G and q be a finite sequence of

elements of the edges of G. Suppose that

(i) lenp 1, (ii) lenq = 1, (iii) (the source of G)(q(1)) = (the target of G)(p(lenp)), (iv) (the source of G)(p(1)) ≠ (the target of G)(p(lenp)), and

(v) it is not true that there exists k such that 1 k and k lenp and (the target of G)(p(k)) = (the target of G)(q(1)). Then p^{⌢} q is a Simple oriented chain of G.

(20) Every Simple oriented chain of G is one-to-one.

5. The Set of the Vertices On a Path or an Edge

Let G be a graph and let e be an element of the edges of G. The functor verticese is defined as follows:

(Def. 1) verticese = {(the source of G)(e), (the target of G)(e)}.

Let us consider G, p_{1}. The functor verticesp_{1} yields a subset of the vertices of G and is defined by:

(Def. 2) verticesp_{1} = {v; v ranges over vertices of G: ⋁_{i} (i ∈ domp_{1} ∧ v ∈

vertices((p_{1})_{i}))}. We now state several propositions:

(21) Let p be a Simple oriented chain of G. Suppose p = p_{1}^{⌢}q_{1} and lenp_{1} 1 and lenq_{1} 1 and (the source of G)(p(1)) ≠ (the target of G)(p(lenp)). Then (the source of G)(p(1)) ∉ verticesq_{1} and (the target of G)(p(lenp)) ∉ verticesp_{1}.

(22) verticesp_{1} ⊆ V iff for every i such that i ∈ domp_{1} holds vertices((p_{1})_{i}) ⊆ V.

(23) Suppose verticesp_{1} ⊈ V. Then there exists a natural number i and there exist finite sequences q, r of elements of the edges of G such that i + 1 lenp_{1} and vertices((p_{1})_{i+1}) ⊈ V and lenq = i and p_{1} = q ^{⌢} r and verticesq ⊆ V.

(24) If rngq_{1} ⊆ rngp_{1}, then verticesq_{1} ⊆ verticesp_{1}.

(25) If rngq_{1} ⊆ rngp_{1} and verticesp_{1} \ X ⊆ V, then verticesq_{1} \ X ⊆ V.

(26) If vertices(p_{1}^{⌢}q_{1})\X ⊆ V, then verticesp_{1} \X ⊆ V and verticesq_{1} \X ⊆

V. In the sequel v, v_{1}, v_{2}, v_{3} denote elements of the vertices of G. One can prove the following four propositions:

(27) For every element e of the edges of G such that v = (the source of G)(e) or v = (the target of G)(e) holds v ∈ verticese.

(28) If i ∈ domp_{1} and if v = (the source of G)(p_{1}(i)) or v = (the target of G)(p_{1}(i)), then v ∈ verticesp_{1}.

(29) If lenp_{1} = 1, then verticesp_{1} = vertices((p_{1})_{1}).

(30) verticesp_{1} ⊆ vertices(p_{1} ^{⌢} q_{1}) and verticesq_{1} ⊆ vertices(p_{1} ^{⌢} q_{1}). In the sequel p, q are oriented chains of G. Next we state two propositions:

(31) If p = q ^{⌢} p_{1} and lenq 1 and lenp_{1} = 1, then verticesp = verticesq ∪ {(the target of G)(p_{1}(1))}.

(32) If v ≠ (the source of G)(p(1)) and v ∈ verticesp, then there exists i such that 1 i and i lenp and v = (the target of G)(p(i)).

6. Directed Paths between Two Vertices

Let us consider G, p, v_{1}, v_{2}. We say that p is oriented path from v_{1} to v_{2} if and only if:

(Def. 3) p ≠ ∅ and (the source of G)(p(1)) = v_{1} and (the target of G)(p(lenp)) =

v_{2}. Let us consider G, v_{1}, v_{2}, p, V. We say that p is oriented path from v_{1} to v_{2}

in V if and only if: (Def. 4) p is oriented path from v_{1} to v_{2} and verticesp \ {v_{2}} ⊆ V.

Let G be a graph and let v_{1}, v_{2} be elements of the vertices of G. The functor OrientedPaths(v_{1}, v_{2}) yields a subset of (the edges of G)^{∗} and is defined by:

(Def. 5) OrientedPaths(v_{1}, v_{2}) = {p; p ranges over oriented chains of G: p is orien-

ted path from v_{1} to v_{2}}. Next we state several propositions:

(33) If p is oriented path from v_{1} to v_{2}, then v_{1} ∈ verticesp and v_{2} ∈ verticesp.

(34) x ∈ OrientedPaths(v_{1}, v_{2}) iff there exists p such that p = x and p is oriented path from v_{1} to v_{2}.

(35) If p is oriented path from v_{1} to v_{2} in V and v_{1} ≠ v_{2}, then v_{1} ∈ V.

(36) If p is oriented path from v_{1} to v_{2} in V and V ⊆ U, then p is oriented path from v_{1} to v_{2} in U.

(37) Suppose lenp 1 and p is oriented path from v_{1} to v_{2} and p_{1}(1) orientedly joins v_{2}, v_{3} and lenp_{1} = 1. Then there exists q such that q = p^{⌢} p_{1} and q is oriented path from v_{1} to v_{3}.

(38) Suppose q = p^{⌢} p_{1} and lenp 1 and lenp_{1} = 1 and p is oriented path from v_{1} to v_{2} in V and p_{1}(1) orientedly joins v_{2}, v_{3}. Then q is oriented path from v_{1} to v_{3} in V ∪ {v_{2}}.

7. Acyclic (or Simple) Paths

Let G be a graph, let p be an oriented chain of G, and let v_{1}, v_{2} be elements of the vertices of G. We say that p is acyclic path from v_{1} to v_{2} if and only if:

(Def. 6) p is Simple and oriented path from v_{1} to v_{2}.

Let G be a graph, let p be an oriented chain of G, let v_{1}, v_{2} be elements of the vertices of G, and let V be a set. We say that p is acyclic path from v_{1} to v_{2} in V if and only if:

(Def. 7) p is Simple and oriented path from v_{1} to v_{2} in V.

Let G be a graph and let v_{1}, v_{2} be elements of the vertices of G. The functor AcyclicPaths(v_{1}, v_{2}) yielding a subset of (the edges of G)^{∗} is defined as follows:

(Def. 8) AcyclicPaths(v_{1}, v_{2}) = {p; p ranges over Simple oriented chains of G: p

is acyclic path from v_{1} to v_{2}}. Let G be a graph, let v_{1}, v_{2} be elements of the vertices of G, and let V be

a set. The functor AcyclicPaths(v_{1}, v_{2}, V) yielding a subset of (the edges of G)^{∗} is defined as follows:

(Def. 9) AcyclicPaths(v_{1}, v_{2}, V) = {p; p ranges over Simple oriented chains of G:

p is acyclic path from v_{1} to v_{2} in V }. Let G be a graph and let p be an oriented chain of G. The functor AcyclicPaths(p) yielding a subset of (the edges of G)^{∗} is defined by the con-

dition (Def. 10). (Def. 10) AcyclicPaths(p) = {q; q ranges over Simple oriented chains of G: q ≠

∅ ∧ (the source of G)(q(1)) = (the source of G)(p(1)) ∧ (the target of G)(q(lenq)) = (the target of G)(p(lenp)) ∧ rngq ⊆ rngp}.

Let G be a graph. The functor AcyclicPaths(G) yields a subset of (the edges of G)^{∗} and is defined as follows:

(Def. 11) AcyclicPaths(G) = {q : q ranges over Simple oriented chains of G}.

The following propositions are true:

(39) If p = ∅, then p is not acyclic path from v_{1} to v_{2}.

(40) If p is acyclic path from v_{1} to v_{2}, then p is oriented path from v_{1} to v_{2}.

(41) AcyclicPaths(v_{1}, v_{2}) ⊆ OrientedPaths(v_{1}, v_{2}).

(42) AcyclicPaths(p) ⊆ AcyclicPaths(G).

(43) AcyclicPaths(v_{1}, v_{2}) ⊆ AcyclicPaths(G).

(44) If p is oriented path from v_{1} to v_{2}, then AcyclicPaths(p) ⊆ AcyclicPaths(v_{1}, v_{2}).

(45) If p is oriented path from v_{1} to v_{2} in V, then AcyclicPaths(p) ⊆ AcyclicPaths(v_{1}, v_{2}, V).

(46) If q ∈ AcyclicPaths(p), then lenq lenp.

(47) If p is oriented path from v_{1} to v_{2}, then AcyclicPaths(p) ≠ ∅ and AcyclicPaths(v_{1}, v_{2}) ≠ ∅.

(48) If p is oriented path from v_{1} to v_{2} in V, then AcyclicPaths(p) ≠ ∅ and AcyclicPaths(v_{1}, v_{2}, V) ≠ ∅.

(49) AcyclicPaths(v_{1}, v_{2}, V) ⊆ AcyclicPaths(G).

8. Weight Graphs and Their Basic Properties

The subset ℝ_{0} of ℝ is defined by: (Def. 12) ℝ_{0} = {r; r ranges over real numbers: r 0}.

Let us mention that ℝ_{0} is non empty. Let G be a graph and let W be a function. We say that W is nonnegative

weight of G if and only if: (Def. 13) W is a function from the edges of G into ℝ_{0} .

Let G be a graph and let W be a function. We say that W is weight of G if and only if:

(Def. 14) W is a function from the edges of G into ℝ.

Let G be a graph, let p be a finite sequence of elements of the edges of G, and let W be a function. Let us assume that W is weight of G. The functor RealSequence(p, W) yielding a finite sequence of elements of ℝ is defined as follows:

(Def. 15) domp = domRealSequence(p, W) and for every natural number i such

that i ∈ domp holds (RealSequence(p, W))(i) = W (p(i)). Let G be a graph, let p be a finite sequence of elements of the edges of G,

and let W be a function. The functor cost(p, W) yields a real number and is defined as follows:

(Def. 16) cost(p, W) = ∑ RealSequence(p, W).

Next we state a number of propositions:

(50) If W is nonnegative weight of G, then W is weight of G.

(51) Let f be a finite sequence of elements of ℝ. Suppose W is nonnegative weight of G and f = RealSequence(p_{1}, W). Let given i. If i ∈ domf, then f(i) 0.

(52) If rngq_{1} ⊆ rngp_{1} and W is weight of G and i ∈ domq_{1}, then there exists j such that j ∈ domp_{1} and (RealSequence(p_{1}, W))(j) = (RealSequence(q_{1}, W))(i).

(53) If lenq_{1} = 1 and rngq_{1} ⊆ rngp_{1} and W is nonnegative weight of G, then cost(q_{1}, W) cost(p_{1}, W).

(54) If W is nonnegative weight of G, then cost(p_{1}, W) 0.

(55) If p_{1} = ∅ and W is weight of G, then cost(p_{1}, W) = 0.

(56) Let D be a non empty finite subset of (the edges of G)^{∗}. If D = AcyclicPaths(v_{1}, v_{2}), then there exists p_{1} such that p_{1} ∈ D and for every q_{1} such that q_{1} ∈ D holds cost(p_{1}, W) cost(q_{1}, W).

(57) Let D be a non empty finite subset of (the edges of G)^{∗}. If D = AcyclicPaths(v_{1}, v_{2}, V), then there exists p_{1} such that p_{1} ∈ D and for every q_{1} such that q_{1} ∈ D holds cost(p_{1}, W) cost(q_{1}, W).

(58) If W is weight of G, then cost(p_{1} ^{⌢} q_{1}, W) = cost(p_{1}, W) + cost(q_{1}, W).

(59) If q_{1} is one-to-one and rngq_{1} ⊆ rngp_{1} and W is nonnegative weight of G, then cost(q_{1}, W) cost(p_{1}, W).

(60) If p_{1} ∈ AcyclicPaths(p) and W is nonnegative weight of G, then cost(p_{1}, W) cost(p, W).

9. Shortest Paths and Their Basic Properties

Let G be a graph, let v_{1}, v_{2} be vertices of G, let p be an oriented chain of G, and let W be a function. We say that p is shortest path from v_{1} to v_{2} in W if and only if the conditions (Def. 17) are satisfied.

(Def. 17)(i) p is oriented path from v_{1} to v_{2}, and

(ii) for every oriented chain q of G such that q is oriented path from v_{1} to

v_{2} holds cost(p, W) cost(q, W). Let G be a graph, let v_{1}, v_{2} be vertices of G, let p be an oriented chain of

G, let V be a set, and let W be a function. We say that p is shortest path from v_{1} to v_{2} in V w.r.t. W if and only if the conditions (Def. 18) are satisfied.

(Def. 18)(i) p is oriented path from v_{1} to v_{2} in V, and

(ii) for every oriented chain q of G such that q is oriented path from v_{1} to v_{2} in V holds cost(p, W) cost(q, W).

10. Basic Properties of a Graph with Finite Vertices

For simplicity, we adopt the following rules: G is a finite graph, p_{4} is a Simple oriented chain of G, P, Q are oriented chains of G, v_{1}, v_{2}, v_{3} are elements of the vertices of G, and p_{1}, q_{1} are finite sequences of elements of the edges of G.

One can prove the following two propositions:

(61) lenp_{4} the number of vertices of G.

(62) lenp_{4} the number of edges of G.

Let us consider G. Note that AcyclicPaths(G) is finite. Let us consider G, P. Note that AcyclicPaths(P) is finite. Let us consider G, v_{1}, v_{2}. One can verify that AcyclicPaths(v_{1}, v_{2}) is finite. Let us consider G, v_{1}, v_{2}, V. Observe that AcyclicPaths(v_{1}, v_{2}, V) is finite. We now state four propositions:

(63) If AcyclicPaths(v_{1}, v_{2}) ≠ ∅, then there exists p_{1} such that p_{1} ∈ AcyclicPaths(v_{1}, v_{2}) and for every q_{1} such that q_{1} ∈ AcyclicPaths(v_{1}, v_{2}) holds cost(p_{1}, W) cost(q_{1}, W).

(64) If AcyclicPaths(v_{1}, v_{2}, V) ≠ ∅, then there exists p_{1} such that p_{1} ∈ AcyclicPaths(v_{1}, v_{2}, V) and for every q_{1} such that q_{1} ∈ AcyclicPaths(v_{1}, v_{2}, V) holds cost(p_{1}, W) cost(q_{1}, W).

(65) If P is oriented path from v_{1} to v_{2} and W is nonnegative weight of G, then there exists a Simple oriented chain of G which is shortest path from v_{1} to v_{2} in W.

(66) Suppose P is oriented path from v_{1} to v_{2} in V and W is nonnegative weight of G. Then there exists a Simple oriented chain of G which is shortest path from v_{1} to v_{2} in V w.r.t. W.

11. Three Basic Theorems for Dijkstra’s Shortest Path Algorithm

We now state two propositions:

(67) Suppose that (i) W is nonnegative weight of G, (ii) P is shortest path from v_{1} to v_{2} in V w.r.t. W, (iii) v_{1} ≠ v_{2}, and (iv) for all Q, v_{3} such that v_{3} ∉ V and Q is shortest path from v_{1} to v_{3} in

V w.r.t. W holds cost(P, W) cost(Q, W). Then P is shortest path from v_{1} to v_{2} in W.

(68) Suppose that (i) W is nonnegative weight of G, (ii) P is shortest path from v_{1} to v_{2} in V w.r.t. W, (iii) v_{1} ≠ v_{2}, (iv) V ⊆ U, and

(v) for all Q, v_{3} such that v_{3} ∉ V and Q is shortest path from v_{1} to v_{3} in V w.r.t. W holds cost(P, W) cost(Q, W). Then P is shortest path from v_{1} to v_{2} in U w.r.t. W.

Let G be a graph, let p_{1} be a finite sequence of elements of the edges of G, let V be a set, let v_{1} be a vertex of G, and let W be a function. We say that p_{1} is longest in shortest path from v_{1} in V w.r.t. W if and only if the condition (Def. 19) is satisfied.

(Def. 19) Let v be a vertex of G. Suppose v ∈ V and v ≠ v_{1}. Then there exists an oriented chain q of G such that q is shortest path from v_{1} to v in V w.r.t. W and cost(q, W) cost(p_{1}, W).

One can prove the following proposition

(69) Let G be a finite oriented graph, P, Q, R be oriented chains of G, and v_{1}, v_{2}, v_{3} be elements of the vertices of G such that e ∈ the edges of G and W is nonnegative weight of G and lenP 1 and P is shortest path from v_{1} to v_{2} in V w.r.t. W and v_{1} ≠ v_{2} and v_{1} ≠ v_{3} and R = P ^{⌢} ⟨e⟩ and Q is shortest path from v_{1} to v_{3} in V w.r.t. W and e orientedly joins v_{2}, v_{3} and P is longest in shortest path from v_{1} in V w.r.t. W. Then

(i) if cost(Q, W) cost(R, W), then Q is shortest path from v_{1} to v_{3} in V ∪ {v_{2}} w.r.t. W, and

(ii) if cost(Q, W) cost(R, W), then R is shortest path from v_{1} to v_{3} in V ∪ {v_{2}} w.r.t. W.

152 jing-chao chen and yatsuka nakamura

References

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[4] Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990.

[5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[6] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[7] Czesław Byliński. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661–668, 1990.

[8] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.

[9] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[10] Krzysztof Hryniewiecki. Graphs. Formalized Mathematics, 2(3):365–370, 1991.

[11] Jarosław Kotowicz and Yatsuka Nakamura. Introduction to Go-board - part I. Formalized Mathematics, 3(1):107–115, 1992.

[12] Yatsuka Nakamura and Piotr Rudnicki. Oriented chains. Formalized Mathematics, 7(2):189–192, 1998.

[13] Andrzej Trybulec. Introduction to arithmetics. To appear in Formalized Mathematics.

[14] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[15] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579, 1990.

[16] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[17] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

On the Hausdorff Distance Between Compact Subsets^{1}

Adam Grabowski University of Białystok

Summary. In [1] the pseudo-metric dist_{min}^{max} on compact subsets A and B of a topological space generated from arbitrary metric space is defined. Using this notion we define the Hausdorff distance (see e.g. [5]) of A and B as a maximum of the two pseudo-distances: from A to B and from B to A. We justify its distance properties. At the end we define some special notions which enable to apply the Hausdorff distance operator “HausDist” to the subsets of the Euclidean topological space E_{T}^{n}.

MML Identifier: HAUSDORF.

The papers [16], [18], [15], [10], [17], [19], [3], [14], [6], [9], [8], [11], [2], [7], [4], [1], [13], and [12] provide the terminology and notation for this paper.

1. Preliminaries

Let r be a real number. Then {r} is a subset of ℝ. Let M be a non empty metric space. One can verify that M_{top} is T_{2}. Next we state a number of propositions:

(1) For all real numbers x, y such that x 0 and y 0 and max(x, y) = 0 holds x = 0.

(2) For every non empty metric space M and for every point x of M holds (dist(x))(x) = 0.

(3) For every non empty metric space M and for every subset P of M_{top} and for every point x of M such that x ∈ P holds 0 ∈ (dist(x))^{∘}P.

1This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102 and TYPES grant IST-1999-29001.

(4) Let M be a non empty metric space, P be a subset of M_{top}, x be a point of M, and y be a real number. If y ∈ (dist(x))^{∘}P, then y 0.

(5) For every non empty metric space M and for every subset P of M_{top} and for every set x such that x ∈ P holds (dist_{min}(P))(x) = 0.

(6) Let M be a non empty metric space, p be a point of M, q be a point of M_{top}, and r be a real number. If p = q and r > 0, then Ball(p, r) is a neighbourhood of q.

(7) Let M be a non empty metric space, A be a subset of M_{top}, and p be a point of M. Then p ∈ \overline{A} if and only if for every real number r such that r > 0 holds Ball(p, r) meets A.

(8) Let M be a non empty metric space, p be a point of M, and A be a subset of M_{top}. Then p ∈ \overline{A} if and only if for every real number r such that r > 0 there exists a point q of M such that q ∈ A and ρ(p, q) < r.

(9) Let M be a non empty metric space, P be a non empty subset of M_{top}, and x be a point of M. Then (dist_{min}(P))(x) = 0 if and only if for every real number r such that r > 0 there exists a point p of M such that p ∈ P and ρ(x, p) < r.

(10) Let M be a non empty metric space, P be a non empty subset of M_{top}, and x be a point of M. Then x ∈ \overline{P} if and only if (dist_{min}(P))(x) = 0.

(11) Let M be a non empty metric space, P be a non empty closed subset of M_{top}, and x be a point of M. Then x ∈ P if and only if (dist_{min}(P))(x) = 0.

(12) For every non empty subset A of the carrier of ℝ^{1} there exists a non empty subset X of ℝ such that A = X and inf A = inf X.

(13) For every non empty subset A of the carrier of ℝ^{1} there exists a non empty subset X of ℝ such that A = X and supA = supX.

(14) Let M be a non empty metric space, P be a non empty subset of M_{top}, x be a point of M, and X be a subset of ℝ. If X = (dist(x))^{∘}P, then X is lower bounded.

(15) Let M be a non empty metric space, P be a non empty subset of M_{top}, and x, y be points of M. If y ∈ P, then (dist_{min}(P))(x) ρ(x, y).

(16) Let M be a non empty metric space, P be a non empty subset of M_{top}, r be a real number, and x be a point of M. If for every point y of M such that y ∈ P holds ρ(x, y) r, then (dist_{min}(P))(x) r.

(17) Let M be a non empty metric space, P be a non empty subset of M_{top}, and x, y be points of M. Then (dist_{min}(P))(x) ρ(x, y)+(dist_{min}(P))(y).

(18) Let M be a non empty metric space, P be a subset of the carrier of M_{top}, and Q be a non empty subset of the carrier of M. If P = Q, then M_{top}↾P = (M↾Q)_{top}.

(19) Let M be a non empty metric space, A be a subset of M, B be a non empty subset of the carrier of M, and C be a subset of M↾B. If A ⊆ B

and A = C and C is bounded, then A is bounded.

(20) Let M be a non empty metric space, B be a subset of M, and A be a subset of M_{top}. If A = B and A is compact, then B is bounded.

(21) Let M be a non empty metric space, P be a non empty subset of M_{top}, and z be a point of M. Then there exists a point w of M such that w ∈ P and (dist_{min}(P))(z) ρ(w, z).

Let M be a non empty metric space and let x be a point of M. Note that dist(x) is continuous.

Let M be a non empty metric space and let X be a compact non empty subset of M_{top}. One can check that dist_{max}(X) is continuous and dist_{min}(X) is continuous.

One can prove the following propositions:

(22) Let M be a non empty metric space, P be a non empty subset of M_{top}, and x, y be points of M. If y ∈ P and P is compact, then (dist_{max}(P))(x) ρ(x, y).

(23) Let M be a non empty metric space, P be a non empty subset of M_{top}, and z be a point of M. If P is compact, then there exists a point w of M such that w ∈ P and (dist_{max}(P))(z) ρ(w, z).

(24) Let M be a non empty metric space, P, Q be non empty subsets of M_{top}, and z be a point of M. If P is compact and Q is compact and z ∈ Q, then (dist_{min}(P))(z) dist_{max}^{max}(P, Q).

(25) Let M be a non empty metric space, P, Q be non empty subsets of M_{top}, and z be a point of M. If P is compact and Q is compact and z ∈ Q, then (dist_{max}(P))(z) dist_{max}^{max}(P, Q).

(26) Let M be a non empty metric space, P, Q be non empty subsets of M_{top}, and X be a subset of ℝ. If X = (dist_{max}(P))^{∘}Q and P is compact and Q is compact, then X is upper bounded.

(27) Let M be a non empty metric space, P, Q be non empty subsets of M_{top}, and X be a subset of ℝ. If X = (dist_{min}(P))^{∘}Q and P is compact and Q is compact, then X is upper bounded.

(28) Let M be a non empty metric space, P be a non empty subset of M_{top}, and z be a point of M. If P is compact, then (dist_{min}(P))(z) (dist_{max}(P))(z).

(29) For every non empty metric space M and for every non empty subset P of M_{top} holds (dist_{min}(P))^{∘}P = {0}.

(30) Let M be a non empty metric space and P, Q be non empty subsets of M_{top}. If P is compact and Q is compact, then dist_{min}^{max}(P, Q) 0.

(31) For every non empty metric space M and for every non empty subset P of M_{top} holds dist_{min}^{max}(P, P) = 0.

(32) Let M be a non empty metric space and P, Q be non empty subsets of M_{top}. If P is compact and Q is compact, then dist_{max}^{min}(P, Q) 0.

(33) Let M be a non empty metric space, Q, R be non empty subsets of M_{top}, and y be a point of M. If Q is compact and R is compact and y ∈ Q, then (dist_{min}(R))(y) dist_{min}^{max}(R, Q).

2. The Hausdorff Distance

Let M be a non empty metric space and let P, Q be subsets of M_{top}. The functor HausDist(P, Q) yields a real number and is defined by:

(Def. 1) HausDist(P, Q) = max(dist_{min}^{max}(P, Q), dist_{min}^{max}(Q, P)).

Let us notice that the functor HausDist(P, Q) is commutative.

The following propositions are true:

(34) Let M be a non empty metric space, Q, R be non empty subsets of M_{top}, and y be a point of M. If Q is compact and R is compact and y ∈ Q, then (dist_{min}(R))(y) HausDist(Q, R).

(35) Let M be a non empty metric space and P, Q, R be non empty subsets of M_{top}. If P is compact and Q is compact and R is compact, then dist_{min}^{max}(P, R) HausDist(P, Q) + HausDist(Q, R).

(36) Let M be a non empty metric space and P, Q, R be non empty subsets of M_{top}. If P is compact and Q is compact and R is compact, then dist_{min}^{max}(R, P) HausDist(P, Q) + HausDist(Q, R).

(37) Let M be a non empty metric space and P, Q be non empty subsets of M_{top}. If P is compact and Q is compact, then HausDist(P, Q) 0.

(38) For every non empty metric space M and for every non empty subset P of M_{top} holds HausDist(P, P) = 0.

(39) Let M be a non empty metric space and P, Q be non empty subsets of M_{top}. If P is compact and Q is compact and HausDist(P, Q) = 0, then P = Q.

(40) Let M be a non empty metric space and P, Q, R be non empty subsets of M_{top}. If P is compact and Q is compact and R is compact, then HausDist(P, R) HausDist(P, Q) + HausDist(Q, R).

Let n be a natural number and let P, Q be subsets of the carrier of E_{T}^{n}. The functor dist_{min}^{max}(P, Q) yields a real number and is defined by:

(Def. 2) There exist subsets P′, Q′ of (E^{n})_{top} such that P = P′ and Q = Q′ and

dist_{min}^{max}(P, Q) = dist_{min}^{max}(P′, Q′). Let n be a natural number and let P, Q be subsets of the carrier of E_{T}^{n}. The

functor HausDist(P, Q) yields a real number and is defined by: (Def. 3) There exist subsets P′, Q′ of (E^{n})_{top} such that P = P′ and Q = Q′ and

HausDist(P, Q) = HausDist(P′, Q′).

on the hausdorff distance between compact … 157

Let us note that the functor HausDist(P, Q) is commutative.

In the sequel n denotes a natural number. Next we state four propositions:

(41) For all non empty subsets P, Q of E_{T}^{n} such that P is compact and Q is compact holds HausDist(P, Q) 0.

(42) For every non empty subset P of E_{T}^{n} holds HausDist(P, P) = 0.

(43) For all non empty subsets P, Q of E_{T}^{n} such that P is compact and Q is compact and HausDist(P, Q) = 0 holds P = Q.

(44) For all non empty subsets P, Q, R of E_{T}^{n} such that P is compact and Q is compact and R is compact holds HausDist(P, R) HausDist(P, Q) + HausDist(Q, R).

References

[1] Józef Białas and Yatsuka Nakamura. The theorem of Weierstrass. Formalized Mathematics, 5(3):353–359, 1996.

[2] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481– 485, 1991.

[3] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[4] Czesław Byliński and Piotr Rudnicki. Bounding boxes for compact sets in E^{2}. Formalized Mathematics, 6(3):427–440, 1997.

[5] Akos Csaszar. General Topology. Akademiai Kiado, Budapest, 1978.

[6] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383–386, 1990.

[7] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

[8] Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces - fundamental concepts. Formalized Mathematics, 2(4):605–608, 1991.

[9] Alicia de la Cruz. Totally bounded metric spaces. Formalized Mathematics, 2(4):559–562, 1991.

[10] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[11] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607–610, 1990.

[12] Jarosław Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477–481, 1990.

[13] Beata Padlewska. Locally connected spaces. Formalized Mathematics, 2(1):93–96, 1991.

[14] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[15] Andrzej Trybulec. Introduction to arithmetics. To appear in Formalized Mathematics.

[16] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[17] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

[18] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

Chains on a Grating in Euclidean Space^{1}

Freek Wiedijk University of Nijmegen

Summary. Translation of pages 101, the second half of 102, and 103 of [15].

MML Identifier: CHAIN 1.

The notation and terminology used here are introduced in the following papers: [20], [10], [22], [23], [18], [8], [12], [9], [17], [1], [19], [14], [3], [6], [13], [16], [2], [11], [4], [7], [21], and [5].

1. Preliminaries

We use the following convention: X, x, y, z are sets and n, m, k, k′, d′ are natural numbers.

The following two propositions are true:

(1) For all real numbers x, y such that x < y there exists a real number z such that x < z and z < y.

(2) For all real numbers x, y there exists a real number z such that x < z and y < z.

The scheme FrSet 1 2 deals with a non empty set A, a non empty set B, a binary functor F yielding an element of A, and a binary predicate P, and states that:

{F(x, y); x ranges over elements of B, y ranges over elements of B : P[x, y]} ⊆ A

for all values of the parameters.

Let B be a set and let A be a subset of B. Then 2^{A} is a subset of 2^{B}.

1This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102 and TYPES grant IST-1999-29001.

Let X be a set. A subset of X is an element of 2^{X}. Let d be a real natural number. Let us observe that d is zero if and only if:

(Def. 1) d ≯ 0.

Let d be a natural number. Let us observe that d is zero if and only if: (Def. 2) d 1̸.

Let us note that there exists a natural number which is non zero. In the sequel d denotes a non zero natural number. Let us consider d. Observe that Segd is non empty. In the sequel i, i_{0} denote elements of Segd. Let us consider X. Let us observe that X is trivial if and only if:

(Def. 3) For all x, y such that x ∈ X and y ∈ X holds x = y. Next we state the proposition (4)^{2} {x, y} is trivial iff x = y. Let us observe that there exists a set which is non trivial and finite. Let X be a non trivial set and let Y be a set. Note that X ∪ Y is non trivial

and Y ∪ X is non trivial.

Let us observe that ℝ is non trivial. Let X be a non trivial set. Observe that there exists a subset of X which is

non trivial and finite.

The following proposition is true

(5) If X is trivial and X ∪ {y} is non trivial, then there exists x such that X = {x}.

Now we present two schemes. The scheme NonEmptyFinite deals with a non empty set A, a non empty finite subset B of A, and a unary predicate P, and states that:

P[B] provided the following requirements are met:

• For every element x of A such that x ∈ B holds P[{x}], and

• Let x be an element of A and B be a non empty finite subset of A. If x ∈ B and B ⊆ B and x ∉ B and P[B], then P[B ∪ {x}].

The scheme NonTrivialFinite deals with a non trivial set A, a non trivial finite subset B of A, and a unary predicate P, and states that:

P[B] provided the following conditions are met:

• For all elements x, y of A such that x ∈ B and y ∈ B and x ≠ y holds P[{x, y}], and

• Let x be an element of A and B be a non trivial finite subset of A. If x ∈ B and B ⊆ B and x ∉ B and P[B], then P[B ∪ {x}].

Next we state the proposition (6) \overline{\overline{X}} = 2 iff there exist x, y such that x ∈ X and y ∈ X and x ≠ y and for

2The proposition (3) has been removed.

every z such that z ∈ X holds z = x or z = y. Let X, Y be finite sets. Note that X−. Y is finite. We now state three propositions:

(7) m is even iff n is even iff m + n is even.

(8) Let X, Y be finite sets. Suppose X misses Y. Then cardX is even iff cardY is even if and only if card(X ∪ Y) is even.

(9) For all finite sets X, Y holds cardX is even iff cardY is even iff card(X−. Y) is even.

Let us consider n. Then R^{n} can be characterized by the condition: (Def. 4) For every x holds x ∈ R^{n} iff x is a function from Segn into ℝ.

We adopt the following rules: l, r, l′, r′, x are elements of R^{d}, G_{1} is a non trivial finite subset of ℝ, and l_{1}, r_{1}, l′_{1}, r′_{1}, x_{1} are real numbers.

Let us consider d, x, i. Then x(i) is a real number.

2. Gratings, Cells, Chains, Cycles

Let us consider d. A function from Segd into 2^{ℝ} is said to be a d-dimensional grating if:

(Def. 5) For every i holds it(i) is non trivial and finite.

In the sequel G is a d-dimensional grating. Let us consider d, G, i. Then G(i) is a non trivial finite subset of ℝ. The following propositions are true:

(10) x ∈ ∏ G iff for every i holds x(i) ∈ G(i).

(11) ∏ G is finite.

(12) For every non empty finite subset X of ℝ there exists r_{1} such that r_{1} ∈ X and for every x_{1} such that x_{1} ∈ X holds r_{1} x_{1}.

(13) For every non empty finite subset X of ℝ there exists l_{1} such that l_{1} ∈ X and for every x_{1} such that x_{1} ∈ X holds l_{1} x_{1}.

(14) There exist l_{1}, r_{1} such that l_{1} ∈ G_{1} and r_{1} ∈ G_{1} and l_{1} < r_{1} and for every x_{1} such that x_{1} ∈ G_{1} holds l_{1} ≮ x_{1} or x_{1} ≮ r_{1}.

(15) There exist l_{1}, r_{1} such that l_{1} ∈ G_{1} and r_{1} ∈ G_{1} and r_{1} < l_{1} and for

every x_{1} such that x_{1} ∈ G_{1} holds x_{1} ≮ r_{1} and l_{1} ≮ x_{1}. Let us consider G_{1}. An element of [: ℝ, ℝ:] is called a gap of G_{1} if it satisfies

the condition (Def. 6). (Def. 6) There exist l_{1}, r_{1} such that

(i) it = ⟨⟨l_{1}, r_{1}⟩⟩, (ii) l_{1} ∈ G_{1}, (iii) r_{1} ∈ G_{1}, and (iv) l_{1} < r_{1} and for every x_{1} such that x_{1} ∈ G_{1} holds l_{1} ≮ x_{1} or x_{1} ≮ r_{1} or

r_{1} < l_{1} and for every x_{1} such that x_{1} ∈ G_{1} holds l_{1} ≮ x_{1} and x_{1} ≮ r_{1}. The following propositions are true:

(16) ⟨⟨l_{1}, r_{1}⟩⟩is a gap of G_{1} if and only if the following conditions are satisfied: (i) l_{1} ∈ G_{1}, (ii) r_{1} ∈ G_{1}, and (iii) l_{1} < r_{1} and for every x_{1} such that x_{1} ∈ G_{1} holds l_{1} ≮ x_{1} or x_{1} ≮ r_{1} or

r_{1} < l_{1} and for every x_{1} such that x_{1} ∈ G_{1} holds l_{1} ≮ x_{1} and x_{1} ≮ r_{1}.

(17) If G_{1} = {l_{1}, r_{1}}, then ⟨⟨l′_{1}, r′_{1}⟩⟩ is a gap of G_{1} iff l′_{1} = l_{1} and r′_{1} = r_{1} or l′_{1} = r_{1} and r′_{1} = l_{1}.

(18) If x_{1} ∈ G_{1}, then there exists r_{1} such that ⟨⟨x_{1}, r_{1}⟩⟩ is a gap of G_{1}.

(19) If x_{1} ∈ G_{1}, then there exists l_{1} such that ⟨⟨l_{1}, x_{1}⟩⟩ is a gap of G_{1}.

(20) If ⟨⟨l_{1}, r_{1}⟩⟩ is a gap of G_{1} and ⟨⟨l_{1}, r′_{1}⟩⟩ is a gap of G_{1}, then r_{1} = r′_{1}.

(21) If ⟨⟨l_{1}, r_{1}⟩⟩ is a gap of G_{1} and ⟨⟨l′_{1}, r_{1}⟩⟩ is a gap of G_{1}, then l_{1} = l′_{1}.

(22) If r_{1} < l_{1} and ⟨⟨l_{1}, r_{1}⟩⟩ is a gap of G_{1} and r′_{1} < l′_{1} and ⟨⟨l′_{1}, r′_{1}⟩⟩ is a gap of

G_{1}, then l_{1} = l′_{1} and r_{1} = r′_{1}. Let us consider d, l, r. The functor cell(l, r) yielding a non empty subset of

R^{d} is defined as follows: (Def. 7) cell(l, r) = {x : ⋀_{i} (l(i) x(i) ∧ x(i) r(i)) ∨ ⋁_{i} (r(i) < l(i) ∧ (x(i)

r(i) ∨ l(i) x(i)))}. We now state several propositions:

(23) x ∈ cell(l, r) iff for every i holds l(i) x(i) and x(i) r(i) or there exists i such that r(i) < l(i) but x(i) r(i) or l(i) x(i).

(24) If for every i holds l(i) r(i), then x ∈ cell(l, r) iff for every i holds l(i) x(i) and x(i) r(i).

(25) If there exists i such that r(i) < l(i), then x ∈ cell(l, r) iff there exists i such that r(i) < l(i) but x(i) r(i) or l(i) x(i).

(26) l ∈ cell(l, r) and r ∈ cell(l, r).

(27) cell(x, x) = {x}.

(28) If for every i holds l′(i) r′(i), then cell(l, r) ⊆ cell(l′, r′) iff for every i holds l′(i) l(i) and l(i) r(i) and r(i) r′(i).

(29) If for every i holds r(i) < l(i), then cell(l, r) ⊆ cell(l′, r′) iff for every i holds r(i) r′(i) and r′(i) < l′(i) and l′(i) l(i).

(30) Suppose for every i holds l(i) r(i) and for every i holds r′(i) < l′(i). Then cell(l, r) ⊆ cell(l′, r′) if and only if there exists i such that r(i) r′(i) or l′(i) l(i).

(31) If for every i holds l(i) r(i) or for every i holds l(i) > r(i), then cell(l, r) = cell(l′, r′) iff l = l′ and r = r′.

Let us consider d, G, k. Let us assume that k d. The functor k-cells(G) yields a finite non empty subset of 2^{R^{d}} and is defined by the condition (Def. 8).

(Def. 8) k-cells(G) = {cell(l, r) : ⋁_{X : subset of Seg d} (cardX = k ∧ ⋀_{i} (i ∈ X ∧ l(i) < r(i) ∧ ⟨⟨l(i), r(i)⟩⟩ is a gap of G(i) ∨ i ∉ X ∧ l(i) = r(i) ∧ l(i) ∈ G(i))) ∨ k = d ∧ ⋀_{i} (r(i) < l(i) ∧ ⟨⟨l(i), r(i)⟩⟩ is a gap of G(i))}.

We now state a number of propositions:

(32) Suppose k d. Let A be a subset of R^{d}. Then A ∈ k-cells(G) if and only if there exist l, r such that A = cell(l, r) but there exists a subset X of Segd such that cardX = k and for every i holds i ∈ X and l(i) < r(i) and ⟨⟨l(i), r(i)⟩⟩is a gap of G(i) or i ∉ X and l(i) = r(i) and l(i) ∈ G(i) or k = d and for every i holds r(i) < l(i) and ⟨⟨l(i), r(i)⟩⟩ is a gap of G(i).

(33) Suppose k d. Then cell(l, r) ∈ k-cells(G) if and only if one of the

following conditions is satisfied:

(i) there exists a subset X of Segd such that cardX = k and for every i holds i ∈ X and l(i) < r(i) and ⟨⟨l(i), r(i)⟩⟩ is a gap of G(i) or i ∉ X and l(i) = r(i) and l(i) ∈ G(i), or

(ii) k = d and for every i holds r(i) < l(i) and ⟨⟨l(i), r(i)⟩⟩ is a gap of G(i).

(34) Suppose k d and cell(l, r) ∈ k-cells(G). Then

(i) for every i holds l(i) < r(i) and ⟨⟨l(i), r(i)⟩⟩is a gap of G(i) or l(i) = r(i) and l(i) ∈ G(i), or

(ii) for every i holds r(i) < l(i) and ⟨⟨l(i), r(i)⟩⟩ is a gap of G(i).

(35) If k d and cell(l, r) ∈ k-cells(G), then for every i holds l(i) ∈ G(i) and r(i) ∈ G(i).

(36) If k d and cell(l, r) ∈ k-cells(G), then for every i holds l(i) r(i) or for every i holds r(i) < l(i).

(37) For every subset A of R^{d} holds A ∈ 0-cells(G) iff there exists x such that A = cell(x, x) and for every i holds x(i) ∈ G(i).

(38) cell(l, r) ∈ 0-cells(G) iff l = r and for every i holds l(i) ∈ G(i).

(39) Let A be a subset of R^{d}. Then A ∈ d-cells(G) if and only if there exist l, r such that A = cell(l, r) but for every i holds ⟨⟨l(i), r(i)⟩⟩ is a gap of G(i) but for every i holds l(i) < r(i) or for every i holds r(i) < l(i).

(40) cell(l, r) ∈ d-cells(G) iff for every i holds ⟨⟨l(i), r(i)⟩⟩is a gap of G(i) but for every i holds l(i) < r(i) or for every i holds r(i) < l(i).

(41) Suppose d = d′+ 1. Let A be a subset of R^{d}. Then A ∈ d′-cells(G) if and only if there exist l, r, i_{0} such that A = cell(l, r) and l(i_{0}) = r(i_{0}) and l(i_{0}) ∈ G(i_{0}) and for every i such that i ≠ i_{0} holds l(i) < r(i) and ⟨⟨l(i), r(i)⟩⟩ is a gap of G(i).

(42) Suppose d = d′+1. Then cell(l, r) ∈ d′-cells(G) if and only if there exists i_{0} such that l(i_{0}) = r(i_{0}) and l(i_{0}) ∈ G(i_{0}) and for every i such that i ≠ i_{0} holds l(i) < r(i) and ⟨⟨l(i), r(i)⟩⟩ is a gap of G(i).

(43) Let A be a subset of R^{d}. Then A ∈ 1-cells(G) if and only if there exist l, r, i_{0} such that A = cell(l, r) and l(i_{0}) < r(i_{0}) or d = 1 and r(i_{0}) < l(i_{0}) and ⟨⟨l(i_{0}), r(i_{0})⟩⟩ is a gap of G(i_{0}) and for every i such that i ≠ i_{0} holds l(i) = r(i) and l(i) ∈ G(i).

(44) cell(l, r) ∈ 1-cells(G) if and only if there exists i_{0} such that l(i_{0}) < r(i_{0}) or d = 1 and r(i_{0}) < l(i_{0}) but ⟨⟨l(i_{0}), r(i_{0})⟩⟩ is a gap of G(i_{0}) but for every i such that i ≠ i_{0} holds l(i) = r(i) and l(i) ∈ G(i).

(45) Suppose k d and k′ d and cell(l, r) ∈ k-cells(G) and cell(l′, r′) ∈

k′-cells(G) and cell(l, r) ⊆ cell(l′, r′). Let given i. Then

(i) l(i) = l′(i) and r(i) = r′(i), or (ii) l(i) = l′(i) and r(i) = l′(i), or (iii) l(i) = r′(i) and r(i) = r′(i), or (iv) l(i) r(i) and r′(i) < l′(i) and r′(i) l(i) and r(i) l′(i).

(46) Suppose k < k′ and k′ d and cell(l, r) ∈ k-cells(G) and cell(l′, r′) ∈ k′-cells(G) and cell(l, r) ⊆ cell(l′, r′). Then there exists i such that l(i) = l′(i) and r(i) = l′(i) or l(i) = r′(i) and r(i) = r′(i).

(47) Let X, X′ be subsets of Segd. Suppose that (i) cell(l, r) ⊆ cell(l′, r′), (ii) for every i holds i ∈ X and l(i) < r(i) and ⟨⟨l(i), r(i)⟩⟩ is a gap of G(i)

or i ∉ X and l(i) = r(i) and l(i) ∈ G(i), and (iii) for every i holds i ∈ X′ and l′(i) < r′(i) and ⟨⟨l′(i), r′(i)⟩⟩ is a gap of

G(i) or i ∉ X′ and l′(i) = r′(i) and l′(i) ∈ G(i). Then

(iv) X ⊆ X′,

(v) for every i such that i ∈ X or i ∉ X′ holds l(i) = l′(i) and r(i) = r′(i), and

(vi) for every i such that i ∉ X and i ∈ X′holds l(i) = l′(i) and r(i) = l′(i)

or l(i) = r′(i) and r(i) = r′(i). Let us consider d, G, k. A k-cell of G is an element of k-cells(G). Let us consider d, G, k. A k-chain of G is a subset of k-cells(G). Let us consider d, G, k. The functor 0_{k}G yields a k-chain of G and is defined

as follows: (Def. 9) 0_{k}G = ∅.

Let us consider d, G. The functor ΩG yielding a d-chain of G is defined as follows:

(Def. 10) ΩG = d-cells(G).

Let us consider d, G, k and let C_{1}, C_{2} be k-chains of G. Then C_{1}−. C_{2} is a k-chain of G. We introduce C_{1} + C_{2} as a synonym of C_{1}−. C_{2}.

Let us consider d, G. The infinite cell of G yielding a d-cell of G is defined by:

(Def. 11) There exist l, r such that the infinite cell of G = cell(l, r) and for every

i holds r(i) < l(i) and ⟨⟨l(i), r(i)⟩⟩ is a gap of G(i). We now state two propositions:

(48) If cell(l, r) is a d-cell of G, then cell(l, r) = the infinite cell of G iff for every i holds r(i) < l(i).

(49) cell(l, r) = the infinite cell of G iff for every i holds r(i) < l(i) and ⟨⟨l(i),

r(i)⟩⟩ is a gap of G(i). The scheme ChainInd deals with a non zero natural number A, a A-dimensional

grating B, a natural number C, a C-chain D of B, and a unary predicate P, and states that:

P[D] provided the parameters have the following properties:

• P[0_{C}B],

• For every C-cell A of B such that A ∈ D holds P[{A}], and

• For all C-chains C_{1}, C_{2} of B such that C_{1} ⊆ D and C_{2} ⊆ D and P[C_{1}] and P[C_{2}] holds P[C_{1} + C_{2}].

Let us consider d, G, k and let A be a k-cell of G. The functor A^{⋆} yields a k + 1-chain of G and is defined by:

(Def. 12) A^{⋆} = {B; B ranges over k + 1-cells of G: A ⊆ B}.

Next we state the proposition

(50) For every k-cell A of G and for every k + 1-cell B of G holds B ∈ A^{⋆} iff

A ⊆ B. Let us consider d, G, k and let C be a k + 1-chain of G. The functor ∂C

yielding a k-chain of G is defined as follows: (Def. 13) ∂C = {A; A ranges over k-cells of G: k + 1 d ∧ card(A^{⋆} ∩ C)is odd}.

We introduce Ċ as a synonym of ∂C.

Let us consider d, G, k, let C be a k + 1-chain of G, and let C′ be a k-chain of G. We say that C′ bounds C if and only if:

(Def. 14) C′= ∂C.

The following propositions are true:

(51) For every k-cell A of G and for every k + 1-chain C of G holds A ∈ ∂C iff k + 1 d and card(A^{⋆} ∩ C) is odd.

(52) If k + 1 > d, then for every k + 1-chain C of G holds ∂C = 0_{k}G.

(53) If k + 1 d, then for every k-cell A of G and for every k + 1-cell B of G holds A ∈ ∂{B} iff A ⊆ B.

(54) If d = d′+ 1, then for every d′-cell A of G holds cardA^{⋆} = 2.

(55) For every d-dimensional grating G and for every 0 + 1-cell B of G holds card∂{B} = 2.

(56) ΩG = (0_{d}G)^{c} and 0_{d}G = (ΩG)^{c}.

(57) For every k-chain C of G holds C + 0_{k}G = C.

(58) For every k-chain C of G holds C + C = 0_{k}G.

(59) For every d-chain C of G holds C^{c} = C + ΩG.

(60) ∂0_{k+1}G = 0_{k}G.

(61) For every d′+ 1-dimensional grating G holds ∂ΩG = 0_{d′}G.

(62) For all k + 1-chains C_{1}, C_{2} of G holds ∂(C_{1} + C_{2}) = ∂C_{1} + ∂C_{2}.

(63) For every d′+ 1-dimensional grating G and for every d′+ 1-chain C of G holds ∂(C^{c}) = ∂C.

(64) For every k + 1 + 1-chain C of G holds ∂∂C = 0_{k}G.

Let us consider d, G, k. A k-chain of G is called a k-cycle of G if: (Def. 15) k = 0 and cardit is even or there exists k′such that k = k′+ 1 and there

exists a k′+ 1-chain C of G such that C = it and ∂C = 0_{k′}G. One can prove the following propositions:

(65) For every k + 1-chain C of G holds C is a k + 1-cycle of G iff ∂C = 0_{k}G.

(66) If k > d, then every k-chain of G is a k-cycle of G.

(67) For every 0-chain C of G holds C is a 0-cycle of G iff cardC is even. Let us consider d, G, k and let C be a k + 1-cycle of G. Then ∂C can be

characterized by the condition: (Def. 16) ∂C = 0_{k}G.

Let us consider d, G, k. Then 0_{k}G is a k-cycle of G.

Let us consider d, G. Then ΩG is a d-cycle of G.

Let us consider d, G, k and let C_{1}, C_{2} be k-cycles of G. Then C_{1}−. C_{2} is a k-cycle of G. We introduce C_{1} + C_{2} as a synonym of C_{1}−. C_{2}.

We now state the proposition

(68) For every d-cycle C of G holds C^{c} is a d-cycle of G.

Let us consider d, G, k and let C be a k +1-chain of G. Then ∂C is a k-cycle of G.

3. Groups and Homomorphisms

Let us consider d, G, k. The functor k-Chains(G) yields a strict Abelian group and is defined by the conditions (Def. 17).

(Def. 17)(i) The carrier of k-Chains(G) = 2^{k-cells(G)}, (ii) 0_{k-Chains(G)} = 0_{k}G, and (iii) for all elements A, B of k-Chains(G) and for all k-chains A′, B′ of G

such that A = A′ and B = B′ holds A + B = A′+ B′. Let us consider d, G, k. A k-grchain of G is an element of k-Chains(G). One can prove the following proposition

chains on a grating in euclidean space 167

(69) For every set x holds x is a k-chain of G iff x is a k-grchain of G. Let us consider d, G, k. The functor ∂ yielding a homomorphism from (k +

1)-Chains(G) to k-Chains(G) is defined by: (Def. 18) For every element A of (k + 1)-Chains(G) and for every k + 1-chain A′

of G such that A = A′ holds ∂(A) = ∂A′.

References

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[3] Grzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589–593, 1990.

[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[5] Józef Białas. Group and field definitions. Formalized Mathematics, 1(3):433–439, 1990.

[6] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[7] Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990.

[8] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[9] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[10] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.

[11] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.

[12] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

[13] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[14] Michał Muzalewski. Opposite rings, modules and their morphisms. Formalized Mathematics, 3(1):57–65, 1992.

[15] M. H. A. Newman. Elements of the Topology of Plane Sets of Points. Cambridge University Press, 1951.

[16] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[17] Piotr Rudnicki and Andrzej Trybulec. Abian’s fixed point theorem. Formalized Mathematics, 6(3):335–338, 1997.

[18] Andrzej Trybulec. Introduction to arithmetics. To appear in Formalized Mathematics.

[19] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[20] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[21] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990.

[22] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[23] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

Bessel’s Inequality

Hiroshi Yamazaki Shinshu University

Nagano Yasunari Shidama Shinshu University Nagano Yatsuka Nakamura Shinshu University Nagano

Summary. In this article we defined the operation of a set and proved Bessel’s inequality. In the first section, we defined the sum of all results of an operation, in which the results are given by taking each element of a set. In the second section, we defined Orthogonal Family and Orthonormal Family. In the last section, we proved some properties of operation of set and Bessel’s inequality.

MML Identifier: BHSP 5.

The articles [12], [16], [10], [7], [5], [6], [17], [15], [9], [13], [3], [8], [1], [11], [4], [2], and [14] provide the terminology and notation for this paper.

1. Sum of the Result of Operation with Each Element of a Set

For simplicity, we adopt the following convention: X denotes a real unitary space, x, y, y_{1}, y_{2} denote points of X, i, j denote natural numbers, D_{1} denotes a non empty set, and p_{1}, p_{2} denote finite sequences of elements of D_{1}.

Next we state the proposition

(1) Suppose p_{1} is one-to-one and p_{2} is one-to-one and rngp_{1} = rngp_{2}. Then domp_{1} = domp_{2} and there exists a permutation P of domp_{1} such that p_{2} = p_{1} · P and domP = domp_{1} and rngP = domp_{1}.

Let D_{1} be a non empty set and let f be a binary operation on D_{1}. Let us assume that f is commutative and associative and has a unity. Let Y be a finite subset of D_{1}. The functor f ⊕Y yields an element of D_{1} and is defined as follows:

(Def. 1) There exists a finite sequence p of elements of D_{1} such that p is one-to-

one and rngp = Y and f ⊕ Y = f ⊙ p. Let us consider X and let Y be a finite subset of the carrier of X. The

functor SetopSum(Y, X) is defined as follows:

(Def. 2) SetopSum(Y, X) = \{ \begin{matrix}(the addition of X) ⊕ Y, if Y ≠ ∅, \\ 0_{X}, otherwise. \end{matrix}

Let us consider X, x, let p be a finite sequence, and let us consider i. The functor PO(i, p, x) is defined by:

(Def. 3) PO(i, p, x) = (the scalar product of X)(⟨⟨x, p(i)⟩⟩).

Let D_{2}, D_{1} be non empty sets, let F be a function from D_{1} into D_{2}, and let p be a finite sequence of elements of D_{1}. The functor FuncSeq(F, p) yielding a finite sequence of elements of D_{2} is defined as follows:

(Def. 4) FuncSeq(F, p) = F · p.

Let D_{2}, D_{1} be non empty sets and let f be a binary operation on D_{2}. Let us assume that f is commutative and associative and has a unity. Let Y be a finite subset of D_{1} and let F be a function from D_{1} into D_{2}. Let us assume that Y ⊆ domF. The functor setopfunc(Y, D_{1}, D_{2}, F, f) yielding an element of D_{2} is defined by:

(Def. 5) There exists a finite sequence p of elements of D_{1} such that p is one-to-

one and rngp = Y and setopfunc(Y, D_{1}, D_{2}, F, f) = f ⊙ FuncSeq(F, p). Let us consider X, x and let Y be a finite subset of the carrier of X. The

functor SetopPreProd(x, Y, X) yields a real number and is defined by the condition (Def. 6).

(Def. 6) There exists a finite sequence p of elements of the carrier of X such that (i) p is one-to-one, (ii) rngp = Y, and (iii) there exists a finite sequence q of elements of ℝ such that domq =

domp and for every i such that i ∈ domq holds q(i) = PO(i, p, x) and SetopPreProd(x, Y, X) = +_{ℝ} ⊙ q.

Let us consider X, x and let Y be a finite subset of the carrier of X. The functor SetopProd(x, Y, X) yielding a real number is defined as follows:

(Def. 7) SetopProd(x, Y, X) = \{ \begin{matrix}SetopPreProd(x, Y, X), if Y ≠ ∅, \\ 0, otherwise. \end{matrix}

2. Orthogonal Family and Orthonormal Family

Let us consider X. A subset of the carrier of X is said to be an orthogonal family of X if:

(Def. 8) For all x, y such that x ∈ it and y ∈ it and x ≠ y holds (x|y) = 0. The following proposition is true

(2) ∅ is an orthogonal family of X.

Let us consider X. Observe that there exists an orthogonal family of X which is finite.

Let us consider X. A subset of the carrier of X is said to be an orthonormal family of X if:

(Def. 9) It is an orthogonal family of X and for every x such that x ∈ it holds

(x|x) = 1. One can prove the following proposition

(3) ∅ is an orthonormal family of X. Let us consider X. One can check that there exists an orthonormal family

of X which is finite. The following proposition is true

(4) x = 0_{X} iff for every y holds (x|y) = 0.

3. Bessel’s Inequality

We now state a number of propositions:

(5) ∥x + y∥^{2} + ∥x − y∥^{2} = 2 · ∥x∥^{2} + 2 · ∥y∥^{2}.

(6) If x, y are orthogonal, then ∥x + y∥^{2} = ∥x∥^{2} + ∥y∥^{2}.

(7) Let p be a finite sequence of elements of the carrier of X. Suppose lenp 1 and for all i, j such that i ∈ domp and j ∈ domp and i ≠ j holds (the scalar product of X)(⟨⟨p(i), p(j)⟩⟩) = 0. Let q be a finite sequence of elements of ℝ. Suppose domp = domq and for every i such that i ∈ domq holds q(i) = (the scalar product of X)(⟨⟨p(i), p(i)⟩⟩). Then ((the addition of X ⊙ p)|(the addition of X ⊙ p)) = +_{ℝ} ⊙ q.

(8) Let p be a finite sequence of elements of the carrier of X. Suppose lenp 1. Let q be a finite sequence of elements of ℝ. Suppose domp = domq and for every i such that i ∈ domq holds q(i) = (the scalar product of X)(⟨⟨x, p(i)⟩⟩). Then (x|(the addition of X ⊙ p)) = +_{ℝ} ⊙ q.

(9) Let S be a finite non empty subset of the carrier of X and F be a function from the carrier of X into the carrier of X. Suppose S ⊆ domF and for all y_{1}, y_{2} such that y_{1} ∈ S and y_{2} ∈ S and y_{1} ≠ y_{2} holds (the scalar product of X)(⟨⟨F (y_{1}), F (y_{2})⟩⟩) = 0. Let H be a function from the carrier of X into ℝ. Suppose S ⊆ domH and for every y such that y ∈ S holds H(y) = (the scalar product of X)(⟨⟨F (y), F (y)⟩⟩). Let p be a finite sequence of elements of the carrier of X. Suppose p is one-to-one and rngp = S. Then (the scalar product of X)(⟨⟨the addition of X ⊙ FuncSeq(F, p), the addition of X ⊙ FuncSeq(F, p)⟩⟩) = +_{ℝ} ⊙ FuncSeq(H, p).

(10) Let S be a finite non empty subset of the carrier of X and F be a function from the carrier of X into the carrier of X. Suppose S ⊆ domF. Let H be a function from the carrier of X into ℝ. Suppose S ⊆ domH and for every y such that y ∈ S holds H(y) = (the scalar product of X)(⟨⟨x, F (y)⟩⟩). Let p be a finite sequence of elements of the carrier of X. Suppose p is oneto-one and rngp = S. Then (the scalar product of X)(⟨⟨x, the addition of X ⊙ FuncSeq(F, p)⟩⟩) = +_{ℝ} ⊙ FuncSeq(H, p).

(11) Let given X. Suppose the addition of X is commutative and associative and the addition of X has a unity. Let given x and S be a finite orthonormal family of X. Suppose S is non empty. Let H be a function from the carrier of X into ℝ. Suppose S ⊆ domH and for every y such that y ∈ S holds H(y) = (x|y)^{2}. Let F be a function from the carrier of X into the carrier of X. Suppose S ⊆ domF and for every y such that y ∈ S holds F (y) = (x|y) · y. Then (x| setopfunc(S, the carrier of X, the carrier of X, F, the addition of X)) = setopfunc(S, the carrier of X, ℝ, H, +_{ℝ}).

(12) Let given X. Suppose the addition of X is commutative and associative and the addition of X has a unity. Let given x and S be a finite orthonormal family of X. Suppose S is non empty. Let F be a function from the carrier of X into the carrier of X. Suppose S ⊆ domF and for every y such that y ∈ S holds F (y) = (x|y) · y. Let H be a function from the carrier of X into ℝ. Suppose S ⊆ domH and for every y such that y ∈ S holds H(y) = (x|y)^{2}. Then (setopfunc(S, the carrier of X, the carrier of X, F, the addition of X)| setopfunc(S, the carrier of X, the carrier of X, F, the addition of X)) = setopfunc(S, the carrier of X, ℝ, H, +_{ℝ}).

(13) Let given X. Suppose the addition of X is commutative and associative and the addition of X has a unity. Let given x and S be a finite orthonormal family of X. Suppose S is non empty. Let H be a function from the carrier of X into ℝ. Suppose S ⊆ domH and for every y such that y ∈ S holds H(y) = (x|y)^{2}. Then setopfunc(S, the carrier of X, ℝ, H, +_{ℝ}) ∥x∥^{2}.

(14) Let D_{2}, D_{1} be non empty sets and f be a binary operation on D_{2}. Suppose f is commutative and associative and has a unity. Let Y_{1}, Y_{2} be finite subsets of D_{1}. Suppose Y_{1} misses Y_{2}. Let F be a function from D_{1} into D_{2}. Suppose Y_{1} ⊆ domF and Y_{2} ⊆ domF. Let Z be a finite subset of D_{1}. If Z = Y_{1} ∪ Y_{2}, then setopfunc(Z, D_{1}, D_{2}, F, f) = f(setopfunc(Y_{1}, D_{1}, D_{2}, F, f), setopfunc(Y_{2}, D_{1}, D_{2}, F, f)).

References

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.

[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[3] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[4] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[5] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[6] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.

bessel’s inequality 173

[7] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[8] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[9] Jan Popiołek. Introduction to Banach and Hilbert spaces - part I. Formalized Mathematics, 2(4):511–516, 1991.

[10] Andrzej Trybulec. Introduction to arithmetics. To appear in Formalized Mathematics.

[11] Andrzej Trybulec. Semilattice operations on finite subsets. Formalized Mathematics, 1(2):369–376, 1990.

[12] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[13] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

[14] Wojciech A. Trybulec. Binary operations on finite sequences. Formalized Mathematics, 1(5):979–981, 1990.

[15] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990.

[16] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[17] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

A Representation of Integers by Binary Arithmetics and Addition of Integers

Hisayoshi Kunimune Shinshu University Nagano Yatsuka Nakamura Shinshu University Nagano

Summary. In this article, we introduce the new concept of 2’s complement representation. Natural numbers that are congruent mod n can be represented by the same n bits binary. Using the concept introduced here, negative numbers that are congruent mod n also can be represented by the same n bit binary. We also show some properties of addition of integers using this concept.

MML Identifier: BINARI 4.

The articles [16], [20], [2], [3], [12], [11], [10], [9], [17], [13], [14], [6], [7], [1], [15], [18], [4], [21], [8], [5], and [19] provide the notation and terminology for this paper.

1. Preliminaries

We follow the rules: n denotes a non empty natural number, j, k, l, m denote natural numbers, and g, h, i denote integers.

We now state a number of propositions:

(1) If m > 0, then m · 2 m + 1.

(2) For every natural number m holds 2^{m} m.

(3) For every natural number m holds ⟨\underbrace{0, …, 0}_{m}⟩ + ⟨\underbrace{0, …, 0}_{m}⟩ = ⟨\underbrace{0, …, 0}_{m}⟩.

(4) For every natural number k such that k l and l m holds k = l or k + 1 l and l m.

(5) For every non empty natural number n and for all n-tuples x, y of Boolean such that x = ⟨\underbrace{0, …, 0}_{n}⟩ and y = ⟨\underbrace{0, …, 0}_{n}⟩ holds carry(x, y) =

⟨\underbrace{0, …, 0}_{n}⟩.

(6) For every non empty natural number n and for all n-tuples x, y of

Boolean such that x = ⟨\underbrace{0, …, 0}_{n}⟩ and y = ⟨\underbrace{0, …, 0}_{n}⟩ holds x+y = ⟨\underbrace{0, …, 0}_{n}⟩.

(7) For every non empty natural number n and for every n-tuple F of Boolean such that F = ⟨\underbrace{0, …, 0}_{n}⟩ holds Intval(F) = 0.

(8) If l + m k − 1, then l < k and m < k.

(9) If g h + i and h < 0 and i < 0, then g < h and g < i.

(10) If l + m 2^{n} − 1, then add ovfl(n -BinarySequence(l), n -BinarySequence(m)) = false.

(11) For every non empty natural number n and for all natural numbers l, m such that l + m 2^{n} − 1 holds Absval((n -BinarySequence(l)) + (n -BinarySequence(m))) = l + m.

(12) For every non empty natural number n and for every n-tuple z of Boolean such that z_{n} = true holds Absval(z) 2^{n− ′1}.

(13) If l + m 2^{n− ′1} − 1, then (carry(n -BinarySequence(l), n -BinarySequence(m)))_{n} = false.

(14) For every non empty natural number n such that l +m 2^{n− ′1} −1 holds Intval((n -BinarySequence(l)) + (n -BinarySequence(m))) = l + m.

(15) For every 1-tuple z of Boolean such that z = ⟨true⟩ holds Intval(z) = − 1.

(16) For every 1-tuple z of Boolean such that z = ⟨false⟩ holds Intval(z) = 0.

(17) For every boolean set x holds true ∨ x = true.

(18) For every non empty natural number n holds 0 2^{n− ′1}−1 and − 2^{n− ′1} 0.

(19) For all n-tuples x, y of Boolean such that x = ⟨\underbrace{0, …, 0}_{n}⟩ and y =

⟨\underbrace{0, …, 0}_{n}⟩ holds x and y are summable.

(20) i · n mod n = 0.

2. Majorant Power

Let m, j be natural numbers. The functor MajP(m, j) yielding a natural number is defined as follows:

(Def. 1) 2^{MajP(m,j)} j and MajP(m, j) m and for every natural number k

such that 2^{k} j and k m holds k MajP(m, j). One can prove the following propositions:

(21) If j k, then MajP(m, j) MajP(m, k).

(22) If l m, then MajP(l, j) MajP(m, j).

(23) If m 1, then MajP(m, 1) = m.

(24) If j 2^{m}, then MajP(m, j) = m.

(25) If j > 2^{m}, then MajP(m, j) > m.

3. 2’s Complement

Let m be a natural number and let i be an integer.

The functor 2sComplement(m, i) yields a m-tuple of Boolean and is defined by:

(Def. 2) 2sComplement(m, i) = \{ \begin{matrix}m -BinarySequence(|2^{MajP(m,|i|)} + i|), if i < 0, \\ m -BinarySequence(|i|), otherwise. \end{matrix}

The following propositions are true:

(26) For every natural number m holds 2sComplement(m, 0) = ⟨\underbrace{0, …, 0}_{m}⟩.

(27) For every integer i such that i 2^{n− ′1} − 1 and − 2^{n− ′1} i holds Intval(2sComplement(n, i)) = i.

(28) For all integers h, i such that h 0 and i 0 or h < 0 and i < 0 but h mod 2^{n} = i mod 2^{n} holds 2sComplement(n, h) = 2sComplement(n, i).

(29) For all integers h, i such that h 0 and i 0 or h < 0 and i < 0 but h ≡ i(mod2^{n}) holds 2sComplement(n, h) = 2sComplement(n, i).

(30) For all natural numbers l, m such that l mod 2^{n} = m mod 2^{n} holds n -BinarySequence(l) = n -BinarySequence(m).

(31) For all natural numbers l, m such that l ≡ m(mod2^{n}) holds n -BinarySequence(l) = n -BinarySequence(m).

(32) For every natural number j such that 1 j and j n holds (2sComplement(n + 1, i))_{j} = (2sComplement(n, i))_{j}.

(33) There exists an element x of Boolean such that 2sComplement(m+1, i) = (2sComplement(m, i))^{⌢} ⟨x⟩.

(34) There exists an element x of Boolean such that (m+1) -BinarySequence(l) = (m -BinarySequence(l))^{⌢} ⟨x⟩.

(35) Let n be a non empty natural number. Suppose − 2^{n} h + i and h < 0 and i < 0 and − 2^{n− ′1} h and − 2^{n− ′1} i. Then (carry(2sComplement(n+ 1, h), 2sComplement(n + 1, i)))_{n+1} = true.

178 hisayoshi kunimune and yatsuka nakamura

(36) For every non empty natural number n such that − 2^{n− ′1} h + i and h + i 2^{n− ′1} − 1 and h 0 and i 0 holds Intval(2sComplement(n, h) + 2sComplement(n, i)) = h + i.

(37) Let n be a non empty natural number. Suppose − 2^{(n+1)− ′1} h + i and h + i 2^{(n+1)− ′1} − 1 and h < 0 and i < 0 and − 2^{n− ′1} h and − 2^{n− ′1} i. Then Intval(2sComplement(n + 1, h) + 2sComplement(n + 1, i)) = h + i.

(38) Let n be a non empty natural number. Suppose that − 2^{n− ′1} h and h 2^{n− ′1} − 1 and − 2^{n− ′1} i and i 2^{n− ′1} − 1 and − 2^{n− ′1} h + i and h + i 2^{n− ′1} − 1 and h 0 and i < 0 or h < 0 and i 0. Then Intval(2sComplement(n, h) + 2sComplement(n, i)) = h + i.

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[3] Czesław Byliński. A classical first order language. Formalized Mathematics, 1(4):669–676, 1990.

[4] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[5] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.

[6] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

[7] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[8] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.

[9] Robert Milewski. Binary arithmetics. Binary sequences. Formalized Mathematics, 7(1):23–26, 1998.

[10] Yasuho Mizuhara and Takaya Nishiyama. Binary arithmetics, addition and subtraction of integers. Formalized Mathematics, 5(1):27–29, 1996.

[11] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Formalized Mathematics, 4(1):83–86, 1993.

[12] Konrad Raczkowski and Andrzej Nędzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213–216, 1991.

[13] Konrad Raczkowski and Andrzej Nędzusiak. Series. Formalized Mathematics, 2(4):449– 452, 1991.

[14] Andrzej Trybulec. Introduction to arithmetics. To appear in Formalized Mathematics.

[15] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[16] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990.

[17] Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821–827, 1990.

[18] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579, 1990.

[19] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[20] Edmund Woronowicz. Many–argument relations. Formalized Mathematics, 1(4):733–737, 1990.

[21] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

The Inner Product of Finite Sequences and of Points of n-dimensional Topological

Space

Kanchun Shinshu University Nagano Yatsuka Nakamura Shinshu University Nagano

Summary. First, we define the inner product to finite sequences of real value. Next, we extend it to points of n-dimensional topological space E_{T}^{n}. At the end, orthogonality is introduced to this space.

MML Identifier: EUCLID 2.

The notation and terminology used in this paper are introduced in the following articles: [11], [3], [9], [7], [1], [2], [6], [8], [4], [5], and [10].

1. Preliminaries

For simplicity, we use the following convention: i, n denote natural numbers, x, y, a denote real numbers, v denotes an element of ℝ^{n}, and p, p_{1}, p_{2}, p_{3}, q, q_{1}, q_{2} denote points of E_{T}^{n}.

We now state several propositions:

(1) For every i such that i ∈ Segn holds (v • ⟨\underbrace{0, …, 0}_{n}⟩)(i) = 0.

(2) v • ⟨\underbrace{0, …, 0}_{n}⟩ = ⟨\underbrace{0, …, 0}_{n}⟩.

(3) For every finite sequence x of elements of ℝ holds (− 1) · x = − x.

(4) For all finite sequences x, y of elements of ℝ such that lenx = leny holds x − y = x + − y.

(5) For every finite sequence x of elements of ℝ holds len(− x) = lenx.

(6) For all finite sequences x_{1}, x_{2} of elements of ℝ such that lenx_{1} = lenx_{2} holds len(x_{1} + x_{2}) = lenx_{1}.

(7) For all finite sequences x_{1}, x_{2} of elements of ℝ such that lenx_{1} = lenx_{2} holds len(x_{1} − x_{2}) = lenx_{1}.

(8) For every real number a and for every finite sequence x of elements of ℝ holds len(a · x) = lenx.

(9) For all finite sequences x, y, z of elements of ℝ such that lenx = leny and leny = lenz holds (x + y) • z = x • z + y • z.

2. Inner Product of Finite Sequences

Let x_{1}, x_{2} be finite sequences of elements of ℝ. The functor |(x_{1}, x_{2})| yielding a real number is defined as follows:

(Def. 1) |(x_{1}, x_{2})| = ∑(x_{1} • x_{2}).

Let us observe that the functor |(x_{1}, x_{2})| is commutative.

We now state a number of propositions:

(10) Let y_{1}, y_{2} be finite sequences of elements of ℝ and x_{1}, x_{2} be elements of R^{n}. If x_{1} = y_{1} and x_{2} = y_{2}, then |(y_{1}, y_{2})| = \frac{1}{4} · (|x_{1} + x_{2}|^{2} − |x_{1} − x_{2}|^{2}).

(11) For every finite sequence x of elements of ℝ holds |(x, x)| 0.

(12) For every finite sequence x of elements of ℝ holds |x|^{2} = |(x, x)|.

(13) For every finite sequence x of elements of ℝ holds |x| = \sqrt{|(x, x)|}.

(14) For every finite sequence x of elements of ℝ holds 0 |x|.

(15) For every finite sequence x of elements of ℝ holds |(x, x)| = 0 iff x =

⟨\underbrace{0, …, 0}_{len x}⟩.

(16) For every finite sequence x of elements of ℝ holds |(x, x)| = 0 iff |x| = 0.

(17) For every finite sequence x of elements of ℝ holds |(x, ⟨\underbrace{0, …, 0}_{len x}⟩)| = 0.

(18) For every finite sequence x of elements of ℝ holds |(⟨\underbrace{0, …, 0}_{len x}⟩, x)| = 0.

(19) For all finite sequences x, y, z of elements of ℝ such that lenx = leny and leny = lenz holds |(x + y, z)| = |(x, z)| + |(y, z)|.

(20) For all finite sequences x, y of elements of ℝ and for every real number a such that lenx = leny holds |(a · x, y)| = a · |(x, y)|.

(21) For all finite sequences x, y of elements of ℝ and for every real number a such that lenx = leny holds |(x, a · y)| = a · |(x, y)|.

(22) For all finite sequences x_{1}, x_{2} of elements of ℝ such that lenx_{1} = lenx_{2} holds |(− x_{1}, x_{2})| = − |(x_{1}, x_{2})|.

the inner product of finite sequences … 181

(23) For all finite sequences x_{1}, x_{2} of elements of ℝ such that lenx_{1} = lenx_{2} holds |(x_{1}, − x_{2})| = − |(x_{1}, x_{2})|.

(24) For all finite sequences x_{1}, x_{2} of elements of ℝ such that lenx_{1} = lenx_{2} holds |(− x_{1}, − x_{2})| = |(x_{1}, x_{2})|.

(25) For all finite sequences x_{1}, x_{2}, x_{3} of elements of ℝ such that lenx_{1} = lenx_{2} and lenx_{2} = lenx_{3} holds |(x_{1} − x_{2}, x_{3})| = |(x_{1}, x_{3})| − |(x_{2}, x_{3})|.

(26) Let x, y be real numbers and x_{1}, x_{2}, x_{3} be finite sequences of elements of ℝ. If lenx_{1} = lenx_{2} and lenx_{2} = lenx_{3}, then |(x · x_{1} + y · x_{2}, x_{3})| = x · |(x_{1}, x_{3})| + y · |(x_{2}, x_{3})|.

(27) For all finite sequences x, y_{1}, y_{2} of elements of ℝ such that lenx = leny_{1} and leny_{1} = leny_{2} holds |(x, y_{1} + y_{2})| = |(x, y_{1})| + |(x, y_{2})|.

(28) For all finite sequences x, y_{1}, y_{2} of elements of ℝ such that lenx = leny_{1} and leny_{1} = leny_{2} holds |(x, y_{1} − y_{2})| = |(x, y_{1})| − |(x, y_{2})|.

(29) Let x_{1}, x_{2}, y_{1}, y_{2} be finite sequences of elements of ℝ. If lenx_{1} = lenx_{2} and lenx_{2} = leny_{1} and leny_{1} = leny_{2}, then |(x_{1}+x_{2}, y_{1}+y_{2})| = |(x_{1}, y_{1})|+ |(x_{1}, y_{2})| + |(x_{2}, y_{1})| + |(x_{2}, y_{2})|.

(30) Let x_{1}, x_{2}, y_{1}, y_{2} be finite sequences of elements of ℝ. If lenx_{1} = lenx_{2} and lenx_{2} = leny_{1} and leny_{1} = leny_{2}, then |(x_{1} − x_{2}, y_{1} − y_{2})| = (|(x_{1}, y_{1})| − |(x_{1}, y_{2})| − |(x_{2}, y_{1})|) + |(x_{2}, y_{2})|.

(31) For all finite sequences x, y of elements of ℝ such that lenx = leny holds |(x + y, x + y)| = |(x, x)| + 2 · |(x, y)| + |(y, y)|.

(32) For all finite sequences x, y of elements of ℝ such that lenx = leny holds |(x − y, x − y)| = (|(x, x)| − 2 · |(x, y)|) + |(y, y)|.

(33) For all finite sequences x, y of elements of ℝ such that lenx = leny holds |x + y|^{2} = |x|^{2} + 2 · |(y, x)| + |y|^{2}.

(34) For all finite sequences x, y of elements of ℝ such that lenx = leny holds |x − y|^{2} = (|x|^{2} − 2 · |(y, x)|) + |y|^{2}.

(35) For all finite sequences x, y of elements of ℝ such that lenx = leny holds |x + y|^{2} + |x − y|^{2} = 2 · (|x|^{2} + |y|^{2}).

(36) For all finite sequences x, y of elements of ℝ such that lenx = leny holds |x + y|^{2} − |x − y|^{2} = 4 · |(x, y)|.

(37) For all finite sequences x, y of elements of ℝ such that lenx = leny holds ||(x, y)|| |x| · |y|.

(38) For all finite sequences x, y of elements of ℝ such that lenx = leny holds

|x + y| |x| + |y|.

3. Inner Product of Points of E_{T}^{n}

Let us consider n and let p, q be points of E_{T}^{n}. The functor |(p, q)| yielding a real number is defined as follows:

(Def. 2) There exist finite sequences f, g of elements of ℝ such that f = p and

g = q and |(p, q)| = |(f, g)|. Let us observe that the functor |(p, q)| is commutative.

We now state a number of propositions:

(39) For every natural number n and for all points p_{1}, p_{2} of E_{T}^{n} holds |(p_{1}, p_{2})| = \frac{1}{4} · (|p_{1} + p_{2}|^{2} − |p_{1} − p_{2}|^{2}).

(40) |(p_{1} + p_{2}, p_{3})| = |(p_{1}, p_{3})| + |(p_{2}, p_{3})|.

(41) For every real number x holds |(x · p_{1}, p_{2})| = x · |(p_{1}, p_{2})|.

(42) For every real number x holds |(p_{1}, x · p_{2})| = x · |(p_{1}, p_{2})|.

(43) |(− p_{1}, p_{2})| = − |(p_{1}, p_{2})|.

(44) |(p_{1}, − p_{2})| = − |(p_{1}, p_{2})|.

(45) |(− p_{1}, − p_{2})| = |(p_{1}, p_{2})|.

(46) |(p_{1} − p_{2}, p_{3})| = |(p_{1}, p_{3})| − |(p_{2}, p_{3})|.

(47) |(x · p_{1} + y · p_{2}, p_{3})| = x · |(p_{1}, p_{3})| + y · |(p_{2}, p_{3})|.

(48) |(p, q_{1} + q_{2})| = |(p, q_{1})| + |(p, q_{2})|.

(49) |(p, q_{1} − q_{2})| = |(p, q_{1})| − |(p, q_{2})|.

(50) |(p_{1} + p_{2}, q_{1} + q_{2})| = |(p_{1}, q_{1})| + |(p_{1}, q_{2})| + |(p_{2}, q_{1})| + |(p_{2}, q_{2})|.

(51) |(p_{1} − p_{2}, q_{1} − q_{2})| = (|(p_{1}, q_{1})| − |(p_{1}, q_{2})| − |(p_{2}, q_{1})|) + |(p_{2}, q_{2})|.

(52) |(p + q, p + q)| = |(p, p)| + 2 · |(p, q)| + |(q, q)|.

(53) |(p − q, p − q)| = (|(p, p)| − 2 · |(p, q)|) + |(q, q)|.

(54) |(p, 0_{E_{T}^{n}})| = 0.

(55) |(0_{E_{T}^{n}}, p)| = 0.

(56) |(0_{E_{T}^{n}}, 0_{E_{T}^{n}})| = 0.

(57) |(p, p)| 0.

(58) |(p, p)| = |p|^{2}.

(59) |p| = \sqrt{|(p, p)|}.

(60) 0 |p|.

(61) |0_{E_{T}^{n}}| = 0.

(62) |(p, p)| = 0 iff |p| = 0.

(63) |(p, p)| = 0 iff p = 0_{E_{T}^{n}}.

(64) |p| = 0 iff p = 0_{E_{T}^{n}}.

(65) p ≠ 0_{E_{T}^{n}} iff |(p, p)| > 0.

(66) p ≠ 0_{E_{T}^{n}} iff |p| > 0.

(67) |p + q|^{2} = |p|^{2} + 2 · |(q, p)| + |q|^{2}.

(68) |p − q|^{2} = (|p|^{2} − 2 · |(q, p)|) + |q|^{2}.

(69) |p + q|^{2} + |p − q|^{2} = 2 · (|p|^{2} + |q|^{2}).

(70) |p + q|^{2} − |p − q|^{2} = 4 · |(p, q)|.

the inner product of finite sequences … 183

(71) |(p, q)| = \frac{1}{4} · (|p + q|^{2} − |p − q|^{2}).

(72) |(p, q)| |(p, p)| + |(q, q)|.

(73) For all points p, q of E_{T}^{n} holds ||(p, q)|| |p| · |q|.

(74) |p + q| |p| + |q|.

Let us consider n, p, q. We say that p, q are orthogonal if and only if: (Def. 3) |(p, q)| = 0.

Let us note that the predicate p, q are orthogonal is symmetric.

The following propositions are true:

(75) p, 0_{E_{T}^{n}} are orthogonal.

(76) 0_{E_{T}^{n}}, p are orthogonal.

(77) p, p are orthogonal iff p = 0_{E_{T}^{n}}.

(78) If p, q are orthogonal, then a · p, q are orthogonal.

(79) If p, q are orthogonal, then p, a · q are orthogonal.

(80) If for every q holds p, q are orthogonal, then p = 0_{E_{T}^{n}}.

References

[1] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[2] Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990.

[3] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[4] Czesław Byliński. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661–668, 1990.

[5] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

[6] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[7] Jan Popiołek. Some properties of functions modul and signum. Formalized Mathematics, 1(2):263–264, 1990.

[8] Agnieszka Sakowicz, Jarosław Gryko, and Adam Grabowski. Sequences in E_{T}^{N}. Formalized Mathematics, 5(1):93–96, 1996.

[9] Andrzej Trybulec. Introduction to arithmetics. To appear in Formalized Mathematics.

[10] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

[11] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

Solving Roots of Polynomial Equation of Degree 4 with Real Coefficients

Xiquan Liang Qingdao University of Science and Technology

Summary. In this paper, we describe the definition of the fourth degree algebraic equations and their properties. We clarify the relation between the four roots of this equation and its coefficient. Also, the form of these roots for various conditions is discussed. This solution is known as the Cardano solution.

MML Identifier: POLYEQ 2.

The articles [3], [4], [1], and [2] provide the notation and terminology for this paper.

Let a, b, c, d, e, x be real numbers. The functor Four(a, b, c, d, e, x) is defined by:

(Def. 1) Four(a, b, c, d, e, x) = a · x^{4} + b · x^{3} + c · x^{2} + d · x + e. Let a, b, c, d, e, x be real numbers. Note that Four(a, b, c, d, e, x) is real. One can prove the following propositions:

(1) Let a, c, e, x be real numbers. Suppose a ≠ 0 and e ≠ 0 and c^{2}−4·a·e > 0.

Suppose Four(a, 0, c, 0, e, x) = 0. Then x ≠ 0 but x = \sqrt{\frac{− c+\sqrt{Δ(a,c,e)}}{2·a}} or

x = \sqrt{\frac{− c−\sqrt{Δ(a,c,e)}}{2·a}} or x = − \sqrt{\frac{− c+\sqrt{Δ(a,c,e)}}{2·a}} or x = − \sqrt{\frac{− c−\sqrt{Δ(a,c,e)}}{2·a}} .

(2) Let a, b, c, x, y be real numbers. Suppose a ≠ 0 and y = x + \frac{1}{x}. If Four(a, b, c, b, a, x) = 0, then x ≠ 0 and (a · y^{2} + b · y + c) − 2 · a = 0.

(3) Let a, b, c, x, y be real numbers. Suppose a ≠ 0 and (b^{2}−4·a·c)+8·a^{2} > 0 and y = x+ \frac{1}{x}. Suppose Four(a, b, c, b, a, x) = 0. Let y_{1}, y_{2} be real numbers.

Suppose y_{1} = ^{\frac{− b+\sqrt{(b^{2} −4·a·c)+8·a^{2}}}{2·a}} and y_{2} = ^{\frac{− b−\sqrt{(b^{2} −4·a·c)+8·a^{2}}}{2·a}} . Then x ≠

0 but x = ^{\frac{y_{1}+\sqrt{Δ(1,− y_{1},1)}}{2}} or x = ^{\frac{y_{2}+\sqrt{Δ(1,− y_{2},1)}}{2}} or x = ^{\frac{y_{1}−\sqrt{Δ(1,− y_{1},1)}}{2}} or

x = ^{\frac{y_{2}−\sqrt{Δ(1,− y_{2},1)}}{2}} .

(4) For every real number x holds x^{3} = x^{2} ·x and x^{3}·x = x^{4} and x^{2} ·x^{2} = x^{4}.

(5) For all real numbers x, y such that x + y ≠ 0 holds (x + y)^{4} = (x^{3} + (3 · y · x^{2} + 3 · y^{2} · x) + y^{3}) · x + (x^{3} + (3 · y · x^{2} + 3 · y^{2} · x) + y^{3}) · y.

(6) For all real numbers x, y such that x + y ≠ 0 holds (x + y)^{4} = x^{4} + (4 · y · x^{3} + 6 · y^{2} · x^{2} + 4 · y^{3} · x) + y^{4}.

(7) Let a_{1}, a_{2}, a_{3}, a_{4}, a_{5}, b_{1}, b_{2}, b_{3}, b_{4}, b_{5} be real numbers. Suppose that for every real number x holds Four(a_{1}, a_{2}, a_{3}, a_{4}, a_{5}, x) = Four(b_{1}, b_{2}, b_{3}, b_{4}, b_{5}, x). Then a_{5} = b_{5} and ((a_{1} − a_{2}) + a_{3}) − a_{4} = ((b_{1} − b_{2}) + b_{3}) − b_{4} and a_{1} + a_{2} + a_{3} + a_{4} = b_{1} + b_{2} + b_{3} + b_{4}.

(8) Let a_{1}, a_{2}, a_{3}, a_{4}, a_{5}, b_{1}, b_{2}, b_{3}, b_{4}, b_{5} be real numbers. Suppose that for every real number x holds Four(a_{1}, a_{2}, a_{3}, a_{4}, a_{5}, x) = Four(b_{1}, b_{2}, b_{3}, b_{4}, b_{5}, x). Then a_{1} − b_{1} = b_{3} − a_{3} and a_{2} − b_{2} = b_{4} − a_{4}.

(9) Let a_{1}, a_{2}, a_{3}, a_{4}, a_{5}, b_{1}, b_{2}, b_{3}, b_{4}, b_{5} be real numbers. Suppose that for every real number x holds Four(a_{1}, a_{2}, a_{3}, a_{4}, a_{5}, x) = Four(b_{1}, b_{2}, b_{3}, b_{4}, b_{5}, x). Then a_{1} = b_{1} and a_{2} = b_{2} and a_{3} = b_{3} and a_{4} = b_{4} and a_{5} = b_{5}.

Let a_{1}, x_{1}, x_{2}, x_{3}, x_{4}, x be real numbers. The functor Four0(a_{1}, x_{1}, x_{2}, x_{3}, x_{4}, x) is defined by:

(Def. 2) Four0(a_{1}, x_{1}, x_{2}, x_{3}, x_{4}, x) = a_{1} · ((x − x_{1}) · (x − x_{2}) · (x − x_{3}) · (x − x_{4})). Let a_{1}, x_{1}, x_{2}, x_{3}, x_{4}, x be real numbers. One can verify that Four0(a_{1}, x_{1}, x_{2}, x_{3}, x_{4}, x) is real. One can prove the following propositions:

(10) Let a_{1}, a_{2}, a_{3}, a_{4}, a_{5}, x, x_{1}, x_{2}, x_{3}, x_{4} be real numbers. Suppose a_{1} ≠ 0. Suppose that for every real number x holds Four(a_{1}, a_{2}, a_{3}, a_{4}, a_{5}, x) = Four0(a_{1}, x_{1}, x_{2}, x_{3}, x_{4}, x). Then \frac{a_{1}·x^{4}+a_{2}·x^{3}+a_{3}·x^{2} +a_{4}·x+a_{5}}{a_{1}}= ((x^{2}·x^{2}−(x_{1}+ x_{2} + x_{3}) · (x^{2} · x)) + (x_{1} · x_{3} + x_{2} · x_{3} + x_{1} · x_{2}) · x^{2}) − x_{1} · x_{2} · x_{3} · x − (x − x_{1}) · (x − x_{2}) · (x − x_{3}) · x_{4}.

(11) Let a_{1}, a_{2}, a_{3}, a_{4}, a_{5}, x, x_{1}, x_{2}, x_{3}, x_{4} be real numbers. Suppose a_{1} ≠ 0. Suppose that for every real number x holds Four(a_{1}, a_{2}, a_{3}, a_{4}, a_{5}, x) = Four0(a_{1}, x_{1}, x_{2}, x_{3}, x_{4}, x). Then \frac{a_{1}·x^{4}+a_{2}·x^{3}+a_{3}·x^{2} +a_{4}·x+a_{5}}{a_{1}}= (((x^{4} − (x_{1} + x_{2} + x_{3} + x_{4}) · x^{3}) + (x_{1} · x_{2} + x_{1} · x_{3} + x_{1} · x_{4} + (x_{2} · x_{3} + x_{2} · x_{4}) + x_{3} · x_{4}) · x^{2}) − (x_{1} · x_{2} · x_{3} + x_{1} · x_{2} · x_{4} + x_{1} · x_{3} · x_{4} + x_{2} · x_{3} · x_{4}) · x) + x_{1} · x_{2} · x_{3} · x_{4}.

(12) Let a_{1}, a_{2}, a_{3}, a_{4}, a_{5}, x_{1}, x_{2}, x_{3}, x_{4} be real numbers. Suppose a_{1} ≠ 0 and for every real number x holds Four(a_{1}, a_{2}, a_{3}, a_{4}, a_{5}, x) = Four0(a_{1}, x_{1}, x_{2}, x_{3}, x_{4}, x). Then \frac{a_{2}}{a_{1}} = − (x_{1} + x_{2} + x_{3} + x_{4}) and \frac{a_{3}}{a_{1}} = x_{1} · x_{2} + x_{1} · x_{3} + x_{1} · x_{4} + (x_{2} · x_{3} + x_{2} · x_{4}) + x_{3} · x_{4} and \frac{a_{4}}{a_{1}} = − (x_{1} · x_{2} · x_{3} + x_{1} · x_{2} · x_{4} + x_{1} · x_{3} · x_{4} + x_{2} · x_{3} · x_{4}) and \frac{a_{5}}{a_{1}} = x_{1} · x_{2} · x_{3} · x_{4}.

(13) Let a, k, y be real numbers. Suppose a ≠ 0. Suppose that for every real number x holds x^{4} +a^{4} = k·a·x·(x^{2} +a^{2}). Then (y^{4} −k·y^{3} −k·y)+1 = 0. solving roots of polynomial equation … 187

References

[1] Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887–890, 1990.

[2] Jan Popiołek. Quadratic inequalities. Formalized Mathematics, 2(4):507–509, 1991.

[3] Andrzej Trybulec. Introduction to arithmetics. To appear in Formalized Mathematics.

[4] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

Morphisms Into Chains. Part I

Artur Korniłowicz University of Białystok

Summary. This work is the continuation of formalization of [10]. Items from 2.1 to 2.8 of Chapter 4 are proved.

MML Identifier: WAYBEL35.

The papers [16], [7], [19], [15], [4], [17], [18], [14], [1], [20], [22], [21], [5], [6], [2], [12], [13], [23], [3], [8], [11], and [9] provide the notation and terminology for this paper.

1. Preliminaries

Let X be a set. One can verify that there exists a subset of X which is trivial.

Let X be a trivial set. Note that every subset of X is trivial.

Let L be a 1-sorted structure. One can check that there exists a subset of L which is trivial.

Let L be a relational structure. Note that there exists a subset of L which is trivial.

Let L be a non empty 1-sorted structure. One can check that there exists a subset of L which is non empty and trivial.

Let L be a non empty relational structure. Note that there exists a subset of L which is non empty and trivial.

Next we state three propositions:

(1) For every set X holds ^{⊆} _{X} is reflexive in X.

(2) For every set X holds ^{⊆} _{X} is transitive in X.

(3) For every set X holds ^{⊆} _{X} is antisymmetric in X.

2. Main Part

Let L be a relational structure. Observe that there exists a binary relation on L which is auxiliary(i).

Let L be a transitive relational structure. Observe that there exists a binary relation on L which is auxiliary(i) and auxiliary(ii).

Let L be an antisymmetric relational structure with l.u.b.’s. Observe that there exists a binary relation on L which is auxiliary(iii).

Let L be a non empty lower-bounded antisymmetric relational structure. Note that there exists a binary relation on L which is auxiliary(iv).

Let L be a non empty relational structure and let R be a binary relation on L. We say that R is extra-order if and only if:

(Def. 1) R is auxiliary(i), auxiliary(ii), and auxiliary(iv).

Let L be a non empty relational structure. One can verify that every binary relation on L which is extra-order is also auxiliary(i), auxiliary(ii), and auxiliary(iv) and every binary relation on L which is auxiliary(i), auxiliary(ii), and auxiliary(iv) is also extra-order.

Let L be a non empty relational structure. One can verify that every binary relation on L which is extra-order and auxiliary(iii) is also auxiliary and every binary relation on L which is auxiliary is also extra-order.

Let L be a lower-bounded antisymmetric transitive non empty relational structure. One can check that there exists a binary relation on L which is extraorder.

Let L be a lower-bounded poset with l.u.b.’s and let R be an auxiliary(ii) binary relation on L. The functor R −LowerMap yields a map from L into ⟨LOWERL, ⊆⟩ and is defined as follows:

(Def. 2) For every element x of the carrier of L holds R −LowerMap (x) = ↓↓_{R}x.

Let L be a lower-bounded poset with l.u.b.’s and let R be an auxiliary(ii) binary relation on L. One can verify that R −LowerMap is monotone.

Let L be a 1-sorted structure and let R be a binary relation on the carrier of L. A subset of L is called a strict chain of R if:

(Def. 3) For all sets x, y such that x ∈ it and y ∈ it holds ⟨⟨x, y⟩⟩∈ R or x = y or

⟨⟨y, x⟩⟩∈ R. The following proposition is true

(4) Let L be a 1-sorted structure, C be a trivial subset of L, and R be a binary relation on the carrier of L. Then C is a strict chain of R.

Let L be a non empty 1-sorted structure and let R be a binary relation on the carrier of L. One can check that there exists a strict chain of R which is non empty and trivial.

One can prove the following four propositions:

(5) Let L be an antisymmetric relational structure, R be an auxiliary(i) binary relation on L, C be a strict chain of R, and x, y be elements of the carrier of L. If x ∈ C and y ∈ C and x < y, then ⟨⟨x, y⟩⟩∈ R.

(6) Let L be an antisymmetric relational structure, R be an auxiliary(i) binary relation on L, and x, y be elements of the carrier of L. If ⟨⟨x, y⟩⟩∈ R and ⟨⟨y, x⟩⟩∈ R, then x = y.

(7) Let L be a non empty lower-bounded antisymmetric relational structure, x be an element of the carrier of L, and R be an auxiliary(iv) binary relation on L. Then {⊥_{L}, x} is a strict chain of R.

(8) Let L be a non empty lower-bounded antisymmetric relational structure, R be an auxiliary(iv) binary relation on L, and C be a strict chain of R. Then C ∪ {⊥_{L}} is a strict chain of R.

Let L be a 1-sorted structure, let R be a binary relation on the carrier of L, and let C be a strict chain of R. We say that C is maximal if and only if:

(Def. 4) For every strict chain D of R such that C ⊆ D holds C = D.

Let L be a 1-sorted structure, let R be a binary relation on the carrier of L, and let C be a set. The functor StrictChains(R, C) is defined by:

(Def. 5) For every set x holds x ∈ StrictChains(R, C) iff x is a strict chain of R

and C ⊆ x. Let L be a 1-sorted structure, let R be a binary relation on the carrier of L,

and let C be a strict chain of R. Note that StrictChains(R, C) is non empty.

Let R be a binary relation and let X be a set. We introduce X is inductive w.r.t. R as a synonym of X has the upper Zorn property w.r.t. R.

Next we state several propositions:

(9) Let L be a 1-sorted structure, R be a binary relation on the carrier of L, and C be a strict chain of R. Then StrictChains(R, C) is inductive w.r.t. ^{⊆} _{StrictChains (R,C)} and there exists a set D such that D is maximal in ⊆ _{StrictChains (R,C)} and C ⊆ D.

(10) Let L be a non empty transitive relational structure, C be a non empty subset of the carrier of L, and X be a subset of C. Suppose sup X exists in L and ⨆_{L} X ∈ C. Then sup X exists in sub(C) and ⨆_{L} X = ⨆_{sub(C)} X.

(11) Let L be a non empty poset, R be an auxiliary(i) auxiliary(ii) binary relation on L, C be a non empty strict chain of R, and X be a subset of C. If sup X exists in L and C is maximal, then sup X exists in sub(C).

(12) Let L be a non empty poset, R be an auxiliary(i) auxiliary(ii) binary relation on L, C be a non empty strict chain of R, and X be a subset of C. Suppose inf ↑⨆_{L} X ∩ C exists in L and sup X exists in L and C is maximal. Then ⨆_{sub(C)} X = ⌈−⌉_{L}(↑⨆_{L} X ∩ C) and if ⨆_{L} X ∉ C, then ⨆_{L} X < ⌈−⌉_{L}(↑⨆_{L} X ∩ C).

(13) Let L be a complete non empty poset, R be an auxiliary(i) auxiliary(ii) binary relation on L, and C be a non empty strict chain of R. If C is maximal, then sub(C) is complete.

(14) Let L be a non empty lower-bounded antisymmetric relational structure, R be an auxiliary(iv) binary relation on L, and C be a strict chain of R. If C is maximal, then ⊥_{L} ∈ C.

(15) Let L be a non empty upper-bounded poset, R be an auxiliary(ii) binary relation on L, C be a strict chain of R, and m be an element of the carrier of L. Suppose C is maximal and m is a maximum of C and ⟨⟨m, ⊤_{L}⟩⟩∈ R. Then ⟨⟨⊤_{L}, ⊤_{L}⟩⟩∈ R and m = ⊤_{L}.

Let L be a relational structure, let C be a set, and let R be a binary relation on the carrier of L. We say that R satisfies SIC on C if and only if the condition (Def. 6) is satisfied.

(Def. 6) Let x, z be elements of the carrier of L. Suppose x ∈ C and z ∈ C and ⟨⟨x, z⟩⟩∈ R and x ≠ z. Then there exists an element y of L such that y ∈ C and ⟨⟨x, y⟩⟩∈ R and ⟨⟨y, z⟩⟩∈ R and x ≠ y.

Let L be a relational structure, let R be a binary relation on the carrier of L, and let C be a strict chain of R. We say that C satisfies SIC if and only if:

(Def. 7) R satisfies SIC on C.

We introduce C satisfies the interpolation property and C satisfies the interpolation property as synonyms of C satisfies SIC.

The following proposition is true

(16) Let L be a relational structure, C be a set, and R be an auxiliary(i) binary relation on L. Suppose R satisfies SIC on C. Let x, z be elements of the carrier of L. Suppose x ∈ C and z ∈ C and ⟨⟨x, z⟩⟩∈ R and x ≠ z. Then there exists an element y of L such that y ∈ C and ⟨⟨x, y⟩⟩∈ R and ⟨⟨y, z⟩⟩∈ R and x < y.

Let L be a relational structure and let R be a binary relation on the carrier of L. Note that every strict chain of R which is trivial satisfies also SIC.

Let L be a non empty relational structure and let R be a binary relation on the carrier of L. One can check that there exists a strict chain of R which is non empty and trivial.

Next we state the proposition

(17) Let L be a lower-bounded poset with l.u.b.’s, R be an auxiliary(i) auxiliary(ii) binary relation on L, and C be a strict chain of R. Suppose C is maximal and R satisfies strong interpolation property. Then R satisfies SIC on C.

Let R be a binary relation and let C, y be sets. The functor SetBelow(R, C, y) is defined as follows:

(Def. 8) SetBelow(R, C, y) = R^{−1} ({y}) ∩ C.

The following proposition is true (18) For every binary relation R and for all sets C, x, y holds x ∈

SetBelow(R, C, y) iff ⟨⟨x, y⟩⟩∈ R and x ∈ C. Let L be a 1-sorted structure, let R be a binary relation on the carrier of L,

and let C, y be sets. Then SetBelow(R, C, y) is a subset of L.

Next we state three propositions:

(19) Let L be a relational structure, R be an auxiliary(i) binary relation on L, C be a set, and y be an element of the carrier of L. Then SetBelow(R, C, y) y.

(20) Let L be a reflexive transitive relational structure, R be an auxiliary(ii) binary relation on L, C be a subset of the carrier of L, and x, y be elements of the carrier of L. If x y, then SetBelow(R, C, x) ⊆ SetBelow(R, C, y).

(21) Let L be a relational structure, R be an auxiliary(i) binary relation on L, C be a set, and x be an element of the carrier of L. If x ∈ C and ⟨⟨x, x⟩⟩∈ R and sup SetBelow(R, C, x) exists in L, then x = supSetBelow(R, C, x).

Let L be a relational structure and let C be a subset of L. We say that C is sup-closed if and only if:

(Def. 9) For every subset X of C such that sup X exists in L holds ⨆_{L} X =

⨆_{sub(C)} X. Next we state three propositions:

(22) Let L be a complete non empty poset, R be an extra-order binary relation on L, C be a strict chain of R satisfying SIC, and p, q be elements of the carrier of L. Suppose p ∈ C and q ∈ C and p < q. Then there exists an element y of L such that p < y and ⟨⟨y, q⟩⟩∈ R and y = supSetBelow(R, C, y).

(23) Let L be a lower-bounded non empty poset, R be an extra-order binary

relation on L, and C be a non empty strict chain of R. Suppose that (i) C is sup-closed, (ii) for every element c of the carrier of L such that c ∈ C holds sup

SetBelow(R, C, c) exists in L, and (iii) R satisfies SIC on C.

Let c be an element of the carrier of L. If c ∈ C, then c = supSetBelow(R, C, c).

(24) Let L be a non empty reflexive antisymmetric relational structure, R be an auxiliary(i) binary relation on L, and C be a strict chain of R. Suppose that for every element c of the carrier of L such that c ∈ C holds sup SetBelow(R, C, c) exists in L and c = supSetBelow(R, C, c). Then R satisfies SIC on C.

Let L be a non empty relational structure, let R be a binary relation on the carrier of L, and let C be a set. The functor SupBelow(R, C) is defined by:

(Def. 10) For every set y holds y ∈ SupBelow(R, C) iff y = supSetBelow(R, C, y).

194 artur korniłowicz

Let L be a non empty relational structure, let R be a binary relation on the carrier of L, and let C be a set. Then SupBelow(R, C) is a subset of L.

One can prove the following propositions:

(25) Let L be a non empty reflexive transitive relational structure, R be an auxiliary(i) auxiliary(ii) binary relation on L, and C be a strict chain of R. Suppose that for every element c of L holds sup SetBelow(R, C, c) exists in L. Then SupBelow(R, C) is a strict chain of R.

(26) Let L be a non empty poset, R be an auxiliary(i) auxiliary(ii) binary relation on L, and C be a subset of the carrier of L. Suppose that for every element c of L holds sup SetBelow(R, C, c) exists in L. Then SupBelow(R, C) is sup-closed.

(27) Let L be a complete non empty poset, R be an extra-order binary relation on L, C be a strict chain of R satisfying SIC, and d be an element of the carrier of L. Suppose d ∈ SupBelow(R, C). Then d = ⨆_{L}{b; b ranges over elements of the carrier of L: b ∈ SupBelow(R, C) ∧ ⟨⟨b, d⟩⟩∈ R}.

(28) Let L be a complete non empty poset, R be an extra-order binary relation on L, and C be a strict chain of R satisfying SIC. Then R satisfies SIC on SupBelow(R, C).

(29) Let L be a complete non empty poset, R be an extra-order binary relation on L, C be a strict chain of R satisfying SIC, and a, b be elements of the carrier of L. Suppose a ∈ C and b ∈ C and a < b. Then there exists an element d of L such that d ∈ SupBelow(R, C) and a < d and ⟨⟨d, b⟩⟩∈ R.

References

[1] Grzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719–725, 1991.

[2] Grzegorz Bancerek. Bounds in posets and relational substructures. Formalized Mathematics, 6(1):81–91, 1997.

[3] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93–107, 1997.

[4] Józef Białas. Group and field definitions. Formalized Mathematics, 1(3):433–439, 1990.

[5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[6] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[7] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.

[8] Czesław Byliński. Galois connections. Formalized Mathematics, 6(1):131–143, 1997.

[9] Marek Dudzicz. Representation theorem for finite distributive lattices. Formalized Mathematics, 9(2):261–264, 2001.

[10] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, Berlin, Heidelberg, New York, 1980.

[11] Adam Grabowski. Auxiliary and approximating relations. Formalized Mathematics, 6(2):179–188, 1997.

[12] Adam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Formalized Mathematics, 6(1):117–121, 1997.

[13] Małgorzata Korolkiewicz. Homomorphisms of algebras. Quotient universal algebra. Formalized Mathematics, 4(1):109–113, 1993.

morphisms into chains. part i 195

[14] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[15] Andrzej Trybulec. Introduction to arithmetics. To appear in Formalized Mathematics.

[16] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[17] Wojciech A. Trybulec. Partially ordered sets. Formalized Mathematics, 1(2):313–319, 1990.

[18] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski - Zorn lemma. Formalized Mathematics, 1(2):387–393, 1990.

[19] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[20] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

[21] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.

[22] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Formalized Mathematics, 1(1):85–89, 1990.

[23] Mariusz Żynel and Czesław Byliński. Properties of relational structures, posets, lattices and maps. Formalized Mathematics, 6(1):123–130, 1997.

Propositional Calculus for Boolean Valued Functions. Part VII

Shunichi Kobayashi Matsumoto University Nagano

Summary. In this paper, we proved some elementary propositional calculus formulae for Boolean valued functions.

MML Identifier: BVFUNC25.

The notation and terminology used in this paper have been introduced in the following articles: [4], [3], [2], and [1].

We use the following convention: Y is a non empty set and a, b, c, d are elements of Boolean^{Y}.

The following propositions are true:

(1) ¬(a ⇒ b) = a ∧ ¬b.

(2) ¬b ⇒ ¬a ⇒ a ⇒ b = true(Y).

(3) a ⇒ b = ¬b ⇒ ¬a.

(4) a ⇔ b = ¬a ⇔ ¬b.

(5) a ⇒ b = a ⇒ a ∧ b.

(6) a ⇔ b = a ∨ b ⇒ a ∧ b.

(7) a ⇔ ¬a = false(Y).

(8) a ⇒ b ⇒ c = b ⇒ a ⇒ c.

(9) a ⇒ b ⇒ c = a ⇒ b ⇒ a ⇒ c.

(10) a ⇔ b = a ⊕ ¬b.

(11) a ∧ (b ⊕ c) = a ∧ b ⊕ a ∧ c.

(12) a ⇔ b = ¬(a ⊕ b).

(13) a ⊕ a = false(Y).

(14) a ⊕ ¬a = true(Y).

(15) a ⇒ b ⇒ b ⇒ a = b ⇒ a.

(16) (a ∨ b) ∧ (¬a ∨ ¬b) = ¬a ∧ b ∨ a ∧ ¬b.

(17) a ∧ b ∨ ¬a ∧ ¬b = (¬a ∨ b) ∧ (a ∨ ¬b).

(18) a ⊕ (b ⊕ c) = (a ⊕ b) ⊕ c.

(19) a ⇔ b ⇔ c = a ⇔ b ⇔ c.

(20) ¬¬a ⇒ a = true(Y).

(21) (a ⇒ b) ∧ a ⇒ b = true(Y).

(22) a ⇒ ¬a ⇒ a = true(Y).

(23) ¬a ⇒ a ⇔ a = true(Y).

(24) a ∨ (a ⇒ b) = true(Y).

(25) (a ⇒ b) ∨ (c ⇒ a) = true(Y).

(26) (a ⇒ b) ∨ (¬a ⇒ b) = true(Y).

(27) (a ⇒ b) ∨ (a ⇒ ¬b) = true(Y).

(28) ¬a ⇒ ¬b ⇔ b ⇒ a = true(Y).

(29) a ⇒ b ⇒ a ⇒ c ⇒ b ⇒ b = true(Y).

(30) a ⇒ b = a ⇔ a ∧ b.

(31) a ⇒ b = true(Y) and b ⇒ a = true(Y) iff a = b.

(32) a = ¬a ⇒ a.

(33) a ⇒ a ⇒ b ⇒ a = true(Y).

(34) a = a ⇒ b ⇒ a.

(35) a = (b ⇒ a) ∧ (¬b ⇒ a).

(36) a ∧ b = ¬(a ⇒ ¬b).

(37) a ∨ b = ¬a ⇒ b.

(38) a ∨ b = a ⇒ b ⇒ b.

(39) a ⇒ b ⇒ a ⇒ a = true(Y).

(40) a ⇒ b ⇒ c ⇒ d ⇒ b ⇒ a ⇒ d ⇒ c = true(Y).

(41) (a ⇒ b) ∧ a ∧ c ⇒ b = true(Y).

(42) b ⇒ c ⇒ a ∧ b ⇒ c = true(Y).

(43) a ∧ b ⇒ c ⇒ a ∧ b ⇒ c ∧ b = true(Y).

(44) a ⇒ b ⇒ a ∧ c ⇒ b ∧ c = true(Y).

(45) (a ⇒ b) ∧ (a ∧ c) ⇒ b ∧ c = true(Y).

(46) a ∧ (a ⇒ b) ∧ (b ⇒ c) ⋐ c.

(47) (a ∨ b) ∧ (a ⇒ c) ∧ (b ⇒ c) ⋐ ¬a ⇒ b ∨ c.

Acknowledgments

This research was partially supported by the research funds of the University of Matsumoto. propositional calculus for boolean valued … 199

References

[1] Shunichi Kobayashi and Kui Jia. A theory of Boolean valued functions and partitions. Formalized Mathematics, 7(2):249–254, 1998.

[2] Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1(3):495–500, 1990.

[3] Edmund Woronowicz. Interpretation and satisfiability in the first order logic. Formalized Mathematics, 1(4):739–743, 1990.

[4] Edmund Woronowicz. Many–argument relations. Formalized Mathematics, 1(4):733–737, 1990.

Basic Notions and Properties of Orthoposets^{1}

Markus Moschner^{2} Saarland University

Summary. Orthoposets are defined. The approach is the standard one via order relation similar to common text books on algebra like [8].

MML Identifier: OPOSET 1.

The terminology and notation used in this paper are introduced in the following papers: [11], [13], [5], [3], [4], [15], [14], [16], [12], [9], [7], [10], [2], [6], and [1].

1. General Notions and Properties

In this paper S, X denote non empty sets and R denotes a binary relation on X.

We consider orthorelational structures, extensions of relational structure and ComplStr, as systems

⟨ a carrier, an internal relation, a complement operation ⟩, where the carrier is a set, the internal relation is a binary relation on the carrier, and the complement operation is a unary operation on the carrier.

Let A, B be sets. The functor ∅_{A,B} yields a relation between A and B and is defined as follows:

(Def. 1) ∅_{A,B} = ∅.

The functor Ω_{B}(A) yields a relation between A and B and is defined by: (Def. 2) Ω_{B}(A) = [: A, B:].

1This work has been partially supported by the CALCULEMUS project (FP5 grant HPRN-CT-2000-00102).

2This paper was worked out while the author was visiting the University of Białystok in autumn 2002.

We now state several propositions:

(1) field(id_{X}) = X.

(2) id_{{∅}} = {⟨⟨∅, ∅⟩⟩}.

(3) op_{1} = {⟨⟨∅, ∅⟩⟩}.

(4) Let L be a non empty reflexive antisymmetric relational structure and x, y be elements of L. If x y, then sup{x, y} = y and inf{x, y} = x.

(5) domR ⊆ fieldR and rngR ⊆ fieldR.

(6) For all sets A, B holds field(∅_{A,B}) = ∅. Let Y be a set. Note that there exists a binary relation on Y which is

antisymmetric.

We now state a number of propositions:

(7) If R is reflexive in X, then R is reflexive and fieldR = X.

(8) If R is symmetric in X, then R is symmetric.

(9) If R is symmetric and fieldR ⊆ S, then R is symmetric in S.

(10) If R is antisymmetric and fieldR ⊆ S, then R is antisymmetric in S.

(11) If R is antisymmetric in X, then R is antisymmetric.

(12) If R is transitive and fieldR ⊆ S, then R is transitive in S.

(13) If R is transitive in X, then R is transitive.

(14) If R is asymmetric and fieldR ⊆ S, then R is asymmetric in S.

(15) If R is asymmetric in X, then R is asymmetric.

(16) If R is irreflexive and fieldR ⊆ S, then R is irreflexive in S.

(17) If R is irreflexive in X, then R is irreflexive.

Let X be a set. Observe that every binary relation on X which is equivalence relation-like is also reflexive, symmetric, and transitive.

Let us consider X. One can check that there exists a binary relation on X which is equivalence relation-like.

Let X be a set. Note that there exists a binary relation on X which is irreflexive, asymmetric, and transitive.

The following proposition is true

(18) △_{∅} is antisymmetric.

Let us consider X, R and let C be a unary operation on X. Note that ⟨X, R, C⟩ is non empty.

Let us mention that there exists a orthorelational structure which is non empty and strict.

Let us consider X and let f be a unary operation on X. We say that f is dneg if and only if:

(Def. 3) For every element x of X holds f(f(x)) = x. We introduce f is involutive as a synonym of f is dneg.

One can prove the following two propositions:

(19) op_{1} is dneg.

(20) id_{X} is dneg.

Let O be a non empty orthorelational structure and let f be a map from O into O. We say that f is DNeg if and only if:

(Def. 4) f is dneg.

Let O be a non empty orthorelational structure. Observe that there exists a map from O into O which is DNeg.

The strict orthorelational structure TrivOrthoRelStr is defined as follows: (Def. 5) TrivOrthoRelStr = ⟨{∅}, id_{{∅}}, op_{1}⟩.

We introduce TrivPoset as a synonym of TrivOrthoRelStr. Let us mention that TrivOrthoRelStr is non empty. The strict orthorelational structure TrivAsymOrthoRelStr is defined by:

(Def. 6) TrivAsymOrthoRelStr = ⟨{∅}, ∅_{{∅},{∅}}, op_{1}⟩.

Let us mention that TrivAsymOrthoRelStr is non empty. Let O be a non empty orthorelational structure. We say that O is Dneg if

and only if: (Def. 7) There exists a map f from O into O such that f = the complement

operation of O and f is DNeg. One can prove the following proposition

(21) TrivOrthoRelStr is Dneg.

Let us note that TrivOrthoRelStr is Dneg. Let us observe that there exists a non empty orthorelational structure which

is Dneg.

In the sequel O is a non empty orthorelational structure. Let R_{1}, R_{2} be relational structures and let f be a map from R_{1} into R_{2}. We

say that f is Antitone on R_{1}, R_{2} if and only if: (Def. 8) f is antitone.

Let R be a relational structure and let f be a map from R into R. We say that f is Antitone on R if and only if:

(Def. 9) f is Antitone on R, R.

Let us consider O. We say that O is SubReFlexive if and only if: (Def. 10) The internal relation of O is reflexive.

Let us consider O. We say that O is ReFlexive if and only if: (Def. 11) The internal relation of O is reflexive in the carrier of O.

We now state two propositions:

(22) If O is ReFlexive, then O is SubReFlexive.

(23) TrivOrthoRelStr is ReFlexive.

Let us observe that TrivOrthoRelStr is ReFlexive. One can verify that there exists a non empty orthorelational structure which

is ReFlexive and strict.

Let us consider O. We say that O is SubIrreFlexive if and only if: (Def. 12) The internal relation of O is irreflexive.

We say that O is IrreFlexive if and only if: (Def. 13) The internal relation of O is irreflexive in the carrier of O.

We now state two propositions:

(24) If O is IrreFlexive, then O is SubIrreFlexive.

(25) TrivAsymOrthoRelStr is IrreFlexive.

Let us note that every non empty orthorelational structure which is IrreFlexive is also SubIrreFlexive.

Let us observe that TrivAsymOrthoRelStr is IrreFlexive. Let us note that there exists a non empty orthorelational structure which is

IrreFlexive and strict.

Let us consider O. We say that O is SubSymmetric if and only if: (Def. 14) The internal relation of O is a symmetric binary relation on the carrier

of O. Let us consider O. We say that O is Symmetric if and only if:

(Def. 15) The internal relation of O is symmetric in the carrier of O.

We now state two propositions:

(26) If O is Symmetric, then O is SubSymmetric.

(27) TrivOrthoRelStr is Symmetric.

Let us observe that every non empty orthorelational structure which is Symmetric is also SubSymmetric.

Let us note that there exists a non empty orthorelational structure which is Symmetric and strict.

Let us consider O. We say that O is SubAntisymmetric if and only if: (Def. 16) The internal relation of O is an antisymmetric binary relation on the

carrier of O. Let us consider O. We say that O is Antisymmetric if and only if:

(Def. 17) The internal relation of O is antisymmetric in the carrier of O.

Next we state two propositions:

(28) If O is Antisymmetric, then O is SubAntisymmetric.

(29) TrivOrthoRelStr is Antisymmetric.

Let us observe that every non empty orthorelational structure which is Antisymmetric is also SubAntisymmetric.

One can verify that TrivOrthoRelStr is Symmetric and Antisymmetric.

One can check that there exists a non empty orthorelational structure which is Symmetric, Antisymmetric, and strict.

Let us consider O. We say that O is SubAsymmetric if and only if: (Def. 18) The internal relation of O is an asymmetric binary relation on the carrier

of O. Let us consider O. We say that O is Asymmetric if and only if:

(Def. 19) The internal relation of O is asymmetric in the carrier of O.

One can prove the following two propositions:

(30) If O is Asymmetric, then O is SubAsymmetric.

(31) TrivAsymOrthoRelStr is Asymmetric.

Let us mention that every non empty orthorelational structure which is Asymmetric is also SubAsymmetric.

One can check that TrivAsymOrthoRelStr is Asymmetric. Let us observe that there exists a non empty orthorelational structure which

is Asymmetric and strict.

Let us consider O. We say that O is SubTransitive if and only if: (Def. 20) The internal relation of O is a transitive binary relation on the carrier

of O. Let us consider O. We say that O is Transitive if and only if:

(Def. 21) The internal relation of O is transitive in the carrier of O.

Next we state two propositions:

(32) If O is Transitive, then O is SubTransitive.

(33) TrivOrthoRelStr is Transitive.

Let us observe that every non empty orthorelational structure which is Transitive is also SubTransitive.

Let us observe that TrivOrthoRelStr is Transitive. Let us observe that there exists a non empty orthorelational structure which

is ReFlexive, Symmetric, Antisymmetric, Transitive, and strict.

Next we state the proposition

(34) TrivAsymOrthoRelStr is Transitive.

Let us mention that TrivAsymOrthoRelStr is IrreFlexive, Asymmetric, and Transitive.

Let us observe that there exists a non empty orthorelational structure which is IrreFlexive, Asymmetric, Transitive, and strict.

Next we state four propositions:

(35) If O is SubSymmetric and SubTransitive, then O is SubReFlexive.

(36) If O is SubIrreFlexive and SubTransitive, then O is SubAsymmetric.

(37) If O is SubAsymmetric, then O is SubIrreFlexive.

(38) If O is ReFlexive and SubSymmetric, then O is Symmetric.

One can check that every non empty orthorelational structure which is Re-Flexive and SubSymmetric is also Symmetric.

Next we state the proposition

(39) If O is ReFlexive and SubAntisymmetric, then O is Antisymmetric. Let us note that every non empty orthorelational structure which is ReFle-

xive and SubAntisymmetric is also Antisymmetric.

The following proposition is true

(40) If O is ReFlexive and SubTransitive, then O is Transitive. Let us note that every non empty orthorelational structure which is ReFle-

xive and SubTransitive is also Transitive.

One can prove the following proposition

(41) If O is IrreFlexive and SubTransitive, then O is Transitive. Let us observe that every non empty orthorelational structure which is Irre-

Flexive and SubTransitive is also Transitive.

Next we state the proposition

(42) If O is IrreFlexive and SubAsymmetric, then O is Asymmetric. Let us note that every non empty orthorelational structure which is IrreFle-

xive and SubAsymmetric is also Asymmetric.

2. Basic Poset Notions

Let us consider O. We say that O is SubQuasiOrdered if and only if: (Def. 22) O is SubReFlexive and SubTransitive.

We introduce O is SubQuasiordered, O is SubPreOrdered, O is SubPreordered, and O is Subpreordered as synonyms of O is SubQuasiOrdered.

Let us consider O. We say that O is QuasiOrdered if and only if: (Def. 23) O is ReFlexive and Transitive.

We introduce O is Quasiordered, O is PreOrdered, and O is Preordered as synonyms of O is QuasiOrdered.

The following proposition is true

(43) If O is QuasiOrdered, then O is SubQuasiOrdered.

Let us observe that every non empty orthorelational structure which is QuasiOrdered is also SubQuasiOrdered.

Let us note that TrivOrthoRelStr is QuasiOrdered. Let us consider O. We say that O is QuasiPure if and only if:

(Def. 24) O is Dneg and QuasiOrdered.

Let us mention that there exists a non empty orthorelational structure which is QuasiPure, Dneg, QuasiOrdered, and strict.

Let us note that TrivOrthoRelStr is QuasiPure.

A QuasiPureOrthoRelStr is a QuasiPure non empty orthorelational structure.

Let us consider O. We say that O is SubPartialOrdered if and only if: (Def. 25) O is ReFlexive, SubAntisymmetric, and SubTransitive.

We introduce O is SubPartialordered as a synonym of O is SubPartialOrdered.

Let us consider O. We say that O is PartialOrdered if and only if: (Def. 26) O is ReFlexive, Antisymmetric, and Transitive.

We introduce O is Partialordered as a synonym of O is PartialOrdered.

We now state the proposition

(44) O is SubPartialOrdered iff O is PartialOrdered.

Let us note that every non empty orthorelational structure which is SubPartialOrdered is also PartialOrdered and every non empty orthorelational structure which is PartialOrdered is also SubPartialOrdered.

Let us observe that every non empty orthorelational structure which is PartialOrdered is also ReFlexive, Antisymmetric, and Transitive and every non empty orthorelational structure which is ReFlexive, Antisymmetric, and Transitive is also PartialOrdered.

Let us consider O. We say that O is Pure if and only if: (Def. 27) O is Dneg and PartialOrdered.

Let us mention that there exists a non empty orthorelational structure which is Pure, Dneg, PartialOrdered, and strict.

One can check that TrivOrthoRelStr is Pure. A PureOrthoRelStr is a Pure non empty orthorelational structure. Let us consider O. We say that O is SubStrictPartialOrdered if and only if:

(Def. 28) O is SubAsymmetric and SubTransitive.

Let us consider O. We say that O is StrictPartialOrdered if and only if: (Def. 29) O is Asymmetric and Transitive.

We introduce O is Strictpartialordered, O is StrictOrdered, and O is Strictordered as synonyms of O is StrictPartialOrdered.

The following proposition is true

(45) If O is StrictPartialOrdered, then O is SubStrictPartialOrdered. Let us note that every non empty orthorelational structure which is Strict-

PartialOrdered is also SubStrictPartialOrdered.

One can prove the following proposition

(46) If O is SubStrictPartialOrdered, then O is SubIrreFlexive. Let us note that every non empty orthorelational structure which is Sub-

StrictPartialOrdered is also SubIrreFlexive.

Next we state the proposition (47) If O is IrreFlexive and SubStrictPartialOrdered, then O is StrictPartia-

lOrdered. Let us mention that every non empty orthorelational structure which is

IrreFlexive and SubStrictPartialOrdered is also StrictPartialOrdered.

We now state the proposition

(48) If O is StrictPartialOrdered, then O is IrreFlexive.

Let us note that every non empty orthorelational structure which is Strict-PartialOrdered is also IrreFlexive.

One can check that TrivAsymOrthoRelStr is IrreFlexive and StrictPartialOrdered.

Let us mention that there exists a non empty strict orthorelational structure which is IrreFlexive and StrictPartialOrdered.

In the sequel P_{1} denotes a PartialOrdered non empty orthorelational structure and Q_{1} denotes a QuasiOrdered non empty orthorelational structure.

We now state the proposition

(49) If Q_{1} is SubAntisymmetric, then Q_{1} is PartialOrdered.

Let P_{1} be a PartialOrdered non empty orthorelational structure. Note that the internal relation of P_{1} is ordering.

One can prove the following proposition

(50) P_{1} is a poset.

Let us note that every non empty orthorelational structure which is PartialOrdered is also reflexive, transitive, and antisymmetric.

Let P_{2}, P_{3} be PartialOrdered non empty orthorelational structures and let f be a map from P_{2} into P_{3}. We say that f is Antitone on P_{2}, P_{3} if and only if:

(Def. 30) f is antitone.

Let P_{1} be a PartialOrdered non empty orthorelational structure and let f be a map from P_{1} into P_{1}. We say that f is Antitone on P_{1} if and only if:

(Def. 31) f is Antitone on P_{1}, P_{1}.

Let P_{2}, P_{3} be PartialOrdered non empty orthorelational structures and let f be a map from P_{2} into P_{3}. We say that f is Antitone if and only if:

(Def. 32) f is Antitone on P_{2}, P_{3}.

Let P_{1} be a PartialOrdered non empty orthorelational structure. Note that there exists a map from P_{1} into P_{1} which is Antitone.

Let us consider P_{1} and let f be a unary operation on the carrier of P_{1}. We say that f is Orderinvolutive if and only if:

(Def. 33) f is a DNeg map from P_{1} into P_{1} and an Antitone map from P_{1} into P_{1}.

Let us consider P_{1}. We say that P_{1} is OrderInvolutive if and only if: (Def. 34) There exists a map f from P_{1} into P_{1} such that f = the complement

operation of P_{1} and f is Orderinvolutive.

Next we state the proposition

(51) The complement operation of TrivOrthoRelStr is Orderinvolutive. Let us observe that TrivOrthoRelStr is OrderInvolutive. One can check that there exists a PartialOrdered non empty orthorelational

structure which is OrderInvolutive and Pure.

A PreOrthoPoset is an OrderInvolutive Pure PartialOrdered non empty orthorelational structure.

Let us consider P_{1} and let f be a unary operation on the carrier of P_{1}. We say that f is QuasiOrthoComplement on P_{1} if and only if:

(Def. 35) f is Orderinvolutive and for every element y of P_{1} holds sup {y, f(y)}

exists in P_{1} and inf {y, f(y)} exists in P_{1}. Let us consider P_{1}. We say that P_{1} is QuasiOrthocomplemented if and only

if: (Def. 36) There exists a map f from P_{1} into P_{1} such that f = the complement

operation of P_{1} and f is QuasiOrthoComplement on P_{1}. Next we state the proposition

(52) TrivOrthoRelStr is QuasiOrthocomplemented.

Let us consider P_{1} and let f be a unary operation on the carrier of P_{1}. We say that f is OrthoComplement on P_{1} if and only if the conditions (Def. 37) are satisfied.

(Def. 37)(i) f is Orderinvolutive, and

(ii) for every element y of P_{1} holds sup {y, f(y)} exists in P_{1} and inf {y, f(y)} exists in P_{1} and ⨆_{P_{1}}{y, f(y)} is a maximum of the carrier of P_{1} and ⌈−⌉_{P_{1}}{y, f(y)} is a minimum of the carrier of P_{1}.

We introduce f is OCompl on P_{1} as a synonym of f is OrthoComplement on P_{1}.

Let us consider P_{1}. We say that P_{1} is Orthocomplemented if and only if: (Def. 38) There exists a map f from P_{1} into P_{1} such that f = the complement

operation of P_{1} and f is OrthoComplement on P_{1}. We introduce P_{1} is Ocompl as a synonym of P_{1} is Orthocomplemented.

Next we state two propositions:

(53) Let f be a unary operation on the carrier of P_{1}. If f is OrthoComplement on P_{1}, then f is QuasiOrthoComplement on P_{1}.

(54) TrivOrthoRelStr is Orthocomplemented.

One can check that TrivOrthoRelStr is QuasiOrthocomplemented and Orthocomplemented.

Let us mention that there exists a PartialOrdered non empty orthorelational structure which is Orthocomplemented and QuasiOrthocomplemented.

210 markus moschner

A QuasiOrthoPoset is a QuasiOrthocomplemented PartialOrdered non empty orthorelational structure. An orthoposet is an Orthocomplemented PartialOrdered non empty orthorelational structure.

References

[1] Grzegorz Bancerek. Bounds in posets and relational substructures. Formalized Mathematics, 6(1):81–91, 1997.

[2] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93–107, 1997.

[3] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[4] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[5] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.

[6] Czesław Byliński. Galois connections. Formalized Mathematics, 6(1):131–143, 1997.

[7] Adam Grabowski. Robbins algebras vs. Boolean algebras. Formalized Mathematics, 9(4):681–690, 2001.

[8] George Grätzer. General Lattice Theory. Academic Press, New York, 1978.

[9] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3–11, 1991.

[10] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[11] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[12] Wojciech A. Trybulec. Partially ordered sets. Formalized Mathematics, 1(2):313–319, 1990.

[13] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[14] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

[15] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.

[16] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Formalized Mathematics, 1(1):85–89, 1990.

basic notions and properties of orthoposets 211

alalalalalal alalalalalalal

Index of MML Identifiers

armstrng . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 bhsp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169 bilinear . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 binari 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .175 bvfunc25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 197 chain 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 159 convex1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .53 euclid 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .179 graph 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143 hausdorf . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 hermitan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 necklace . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 oposet 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .201 pnproc 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .125 polyeq 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .185 polyred . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 radix 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133 radix 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139 rusub 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 rusub 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 rusub 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 rusub 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 rusub 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 sin cos3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 termord . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 vectsp10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 waybel35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 189

Contents Formaliz. Math. 11 (2)

Improvement of Radix-2^{k} Signed-Digit Number for High Speed

Circuit

By Masaaki Niimura and Yasushi Fuwa  . . . . . . . . . . . . . . . . . . . 133

High Speed Adder Algorithm with Radix-2^{k} Sub Signed-Digit

Number

By Masaaki Niimura and Yasushi Fuwa  . . . . . . . . . . . . . . . . . . . 139

The Underlying Principle of Dijkstra’s Shortest Path Algorithm

By Jing-Chao Chen and Yatsuka Nakamura  . . . . . . . . . . . . . . 143

On the Hausdorff Distance Between Compact Subsets

By Adam Grabowski . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153

Chains on a Grating in Euclidean Space

By Freek Wiedijk  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 159

Bessel’s Inequality

By Hiroshi Yamazaki et al. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169

A Representation of Integers by Binary Arithmetics and Addition

of Integers

By Hisayoshi Kunimune and Yatsuka Nakamura  . . . . . . . . . 175

The Inner Product of Finite Sequences and of Points of n-

dimensional Topological Space

By Kanchun and Yatsuka Nakamura  . . . . . . . . . . . . . . . . . . . . . 179

Solving Roots of Polynomial Equation of Degree 4 with Real Co-

efficients

By Xiquan Liang . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185

Morphisms Into Chains. Part I

By Artur Korniłowicz  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 189

Propositional Calculus for Boolean Valued Functions. Part VII

By Shunichi Kobayashi  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 197

Continued on inside back cover

Basic Notions and Properties of Orthoposets

By Markus Moschner  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201

Index of MML Identifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 212