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

On the Sets Inhabited by Numbers^{1}

Andrzej Trybulec University of Białystok

Summary. The information that all members of a set enjoy a property expressed by an adjective can be processed in a systematic way. The purpose of the work is to find out how to do that. If it works, ‘membered’ will become a reserved word and the work with it will be automated. I have chosen membered rather than inhabited because of the compatibility with the Automath terminology. The phrase τ inhabits θ could be translated to τ is θ in Mizar.

MML Identifier: MEMBERED.

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

In this paper x, X, F denote sets.

Let X be a set. We say that X is complex-membered if and only if: (Def. 1) If x ∈ X, then x is complex.

We say that X is real-membered if and only if: (Def. 2) If x ∈ X, then x is real.

We say that X is rational-membered if and only if: (Def. 3) If x ∈ X, then x is rational.

We say that X is integer-membered if and only if: (Def. 4) If x ∈ X, then x is integer.

We say that X is natural-membered if and only if: (Def. 5) If x ∈ X, then x is natural.

One can check the following observations:

∗ every set which is natural-membered is also integer-membered,

∗ every set which is integer-membered is also rational-membered, ∗ every set which is rational-membered is also real-membered, and

1This work has been partially supported by the CALCULEMUS grant HPRN-CT-2000-00102.

∗ every set which is real-membered is also complex-membered. Let us observe that there exists a set which is non empty and natural-

membered.

One can verify the following observations:

∗ every subset of ℂ is complex-membered,

∗ every subset of ℝ is real-membered,

∗ every subset of ℚ is rational-membered,

∗ every subset of ℤ is integer-membered, and

∗ every subset of ℕ is natural-membered. One can verify the following observations:

∗ ℂ is complex-membered,

∗ ℝ is real-membered,

∗ ℚ is rational-membered,

∗ ℤ is integer-membered, and

∗ ℕ is natural-membered. Next we state several propositions:

(1) If X is complex-membered, then X ⊆ ℂ.

(2) If X is real-membered, then X ⊆ ℝ.

(3) If X is rational-membered, then X ⊆ ℚ.

(4) If X is integer-membered, then X ⊆ ℤ.

(5) If X is natural-membered, then X ⊆ ℕ. Let X be a complex-membered set. One can check that every element of X

is complex.

Let X be a real-membered set. One can verify that every element of X is real.

Let X be a rational-membered set. Note that every element of X is rational. Let X be an integer-membered set. One can verify that every element of X

is integer.

Let X be a natural-membered set. Observe that every element of X is natural.

For simplicity, we follow the rules: c, c_{1}, c_{2}, c_{3} are complex numbers, r, r_{1}, r_{2}, r_{3} are real numbers, w, w_{1}, w_{2}, w_{3} are rational numbers, i, i_{1}, i_{2}, i_{3} are integer numbers, and n, n_{1}, n_{2}, n_{3} are natural numbers.

We now state a number of propositions:

(6) For every non empty complex-membered set X there exists c such that c ∈ X.

(7) For every non empty real-membered set X there exists r such that r ∈ X.

(8) For every non empty rational-membered set X there exists w such that w ∈ X.

(9) For every non empty integer-membered set X there exists i such that i ∈ X.

(10) For every non empty natural-membered set X there exists n such that n ∈ X.

(11) For every complex-membered set X such that for every c holds c ∈ X holds X = ℂ.

(12) For every real-membered set X such that for every r holds r ∈ X holds X = ℝ.

(13) For every rational-membered set X such that for every w holds w ∈ X holds X = ℚ.

(14) For every integer-membered set X such that for every i holds i ∈ X holds X = ℤ.

(15) For every natural-membered set X such that for every n holds n ∈ X holds X = ℕ.

(16) For every complex-membered set Y such that X ⊆ Y holds X is complexmembered.

(17) For every real-membered set Y such that X ⊆ Y holds X is realmembered.

(18) For every rational-membered set Y such that X ⊆ Y holds X is rationalmembered.

(19) For every integer-membered set Y such that X ⊆ Y holds X is integermembered.

(20) For every natural-membered set Y such that X ⊆ Y holds X is natural-

membered. One can verify that ∅ is natural-membered. One can verify that every set which is empty is also natural-membered. Let us consider c. One can verify that {c} is complex-membered. Let us consider r. One can verify that {r} is real-membered. Let us consider w. One can check that {w} is rational-membered. Let us consider i. One can verify that {i} is integer-membered. Let us consider n. Observe that {n} is natural-membered. Let us consider c_{1}, c_{2}. Note that {c_{1}, c_{2}} is complex-membered. Let us consider r_{1}, r_{2}. One can check that {r_{1}, r_{2}} is real-membered. Let us consider w_{1}, w_{2}. Observe that {w_{1}, w_{2}} is rational-membered. Let us consider i_{1}, i_{2}. One can verify that {i_{1}, i_{2}} is integer-membered. Let us consider n_{1}, n_{2}. Observe that {n_{1}, n_{2}} is natural-membered. Let us consider c_{1}, c_{2}, c_{3}. One can verify that {c_{1}, c_{2}, c_{3}} is complex-membered. Let us consider r_{1}, r_{2}, r_{3}. One can verify that {r_{1}, r_{2}, r_{3}} is real-membered.

Let us consider w_{1}, w_{2}, w_{3}. Observe that {w_{1}, w_{2}, w_{3}} is rational-membered. Let us consider i_{1}, i_{2}, i_{3}. One can verify that {i_{1}, i_{2}, i_{3}} is integer-membered. Let us consider n_{1}, n_{2}, n_{3}. One can check that {n_{1}, n_{2}, n_{3}} is natural-

membered.

Let X be a complex-membered set. Note that every subset of X is complexmembered.

Let X be a real-membered set. One can verify that every subset of X is real-membered.

Let X be a rational-membered set. One can check that every subset of X is rational-membered.

Let X be an integer-membered set. Observe that every subset of X is integermembered.

Let X be a natural-membered set. One can verify that every subset of X is natural-membered.

Let X, Y be complex-membered sets. Note that X∪Y is complex-membered. Let X, Y be real-membered sets. Observe that X ∪ Y is real-membered. Let X, Y be rational-membered sets. Note that X ∪Y is rational-membered. Let X, Y be integer-membered sets. Note that X ∪ Y is integer-membered. Let X, Y be natural-membered sets. Observe that X∪Y is natural-membered. Let X be a complex-membered set and let Y be a set. Note that X ∩ Y is

complex-membered and Y ∩ X is complex-membered.

Let X be a real-membered set and let Y be a set. Note that X ∩ Y is real-membered and Y ∩ X is real-membered.

Let X be a rational-membered set and let Y be a set. Observe that X ∩ Y is rational-membered and Y ∩ X is rational-membered.

Let X be an integer-membered set and let Y be a set. Note that X ∩ Y is integer-membered and Y ∩ X is integer-membered.

Let X be a natural-membered set and let Y be a set. Observe that X ∩ Y is natural-membered and Y ∩ X is natural-membered.

Let X be a complex-membered set and let Y be a set. Note that X \ Y is complex-membered.

Let X be a real-membered set and let Y be a set. Note that X \ Y is realmembered.

Let X be a rational-membered set and let Y be a set. Observe that X \ Y is rational-membered.

Let X be an integer-membered set and let Y be a set. Observe that X \ Y is integer-membered.

Let X be a natural-membered set and let Y be a set. Observe that X \ Y is natural-membered.

Let X, Y be complex-membered sets. Note that X−. Y is complex-membered. Let X, Y be real-membered sets. One can check that X−. Y is real-membered. Let X, Y be rational-membered sets. Note that X−. Y is rational-membered.

Let X, Y be integer-membered sets. One can check that X−. Y is integermembered.

Let X, Y be natural-membered sets. One can verify that X−. Y is naturalmembered.

Let X, Y be complex-membered sets. Let us observe that X ⊆ Y if and only if:

(Def. 6) If c ∈ X, then c ∈ Y.

Let X, Y be real-membered sets. Let us observe that X ⊆ Y if and only if: (Def. 7) If r ∈ X, then r ∈ Y.

Let X, Y be rational-membered sets. Let us observe that X ⊆ Y if and only if:

(Def. 8) If w ∈ X, then w ∈ Y.

Let X, Y be integer-membered sets. Let us observe that X ⊆ Y if and only if:

(Def. 9) If i ∈ X, then i ∈ Y.

Let X, Y be natural-membered sets. Let us observe that X ⊆ Y if and only if:

(Def. 10) If n ∈ X, then n ∈ Y.

Let X, Y be complex-membered sets. Let us observe that X = Y if and only if:

(Def. 11) c ∈ X iff c ∈ Y.

Let X, Y be real-membered sets. Let us observe that X = Y if and only if: (Def. 12) r ∈ X iff r ∈ Y.

Let X, Y be rational-membered sets. Let us observe that X = Y if and only if:

(Def. 13) w ∈ X iff w ∈ Y.

Let X, Y be integer-membered sets. Let us observe that X = Y if and only if:

(Def. 14) i ∈ X iff i ∈ Y.

Let X, Y be natural-membered sets. Let us observe that X = Y if and only if:

(Def. 15) n ∈ X iff n ∈ Y.

Let X, Y be complex-membered sets. Let us observe that X meets Y if and only if:

(Def. 16) There exists c such that c ∈ X and c ∈ Y.

Let X, Y be real-membered sets. Let us observe that X meets Y if and only if:

(Def. 17) There exists r such that r ∈ X and r ∈ Y.

Let X, Y be rational-membered sets. Let us observe that X meets Y if and only if:

(Def. 18) There exists w such that w ∈ X and w ∈ Y.

Let X, Y be integer-membered sets. Let us observe that X meets Y if and only if:

(Def. 19) There exists i such that i ∈ X and i ∈ Y.

Let X, Y be natural-membered sets. Let us observe that X meets Y if and only if:

(Def. 20) There exists n such that n ∈ X and n ∈ Y.

One can prove the following propositions:

(21) If for every X such that X ∈ F holds X is complex-membered, then ⋃ F is complex-membered.

(22) If for every X such that X ∈ F holds X is real-membered, then ⋃ F is real-membered.

(23) If for every X such that X ∈ F holds X is rational-membered, then ⋃ F is rational-membered.

(24) If for every X such that X ∈ F holds X is integer-membered, then ⋃ F is integer-membered.

(25) If for every X such that X ∈ F holds X is natural-membered, then ⋃ F is natural-membered.

(26) For every X such that X ∈ F and X is complex-membered holds ⋂ F is complex-membered.

(27) For every X such that X ∈ F and X is real-membered holds ⋂ F is real-membered.

(28) For every X such that X ∈ F and X is rational-membered holds ⋂ F is rational-membered.

(29) For every X such that X ∈ F and X is integer-membered holds ⋂ F is integer-membered.

(30) For every X such that X ∈ F and X is natural-membered holds ⋂ F is

natural-membered. In this article we present several logical schemes. The scheme CM Separation

concerns a unary predicate P, and states that: There exists a complex-membered set X such that for every c holds c ∈ X iff P[c]

for all values of the parameters.

The scheme RM Separation concerns a unary predicate P, and states that: There exists a real-membered set X such that for every r holds r ∈ X iff P[r]

for all values of the parameters.

The scheme WM Separation concerns a unary predicate P, and states that: There exists a rational-membered set X such that for every w holds w ∈ X iff P[w]

for all values of the parameters.

The scheme IM Separation concerns a unary predicate P, and states that: There exists an integer-membered set X such that for every i holds i ∈ X iff P[i]

for all values of the parameters.

The scheme NM Separation concerns a unary predicate P, and states that: There exists a natural-membered set X such that for every n holds n ∈ X iff P[n]

for all values of the parameters.

Acknowledgments

I am grateful to Dr. Czeslaw Bylinski for the discussion, particularly for his advice to prove more trivial but useful theorems.

References

[1] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.

[2] Grzegorz Bancerek. Sequences of ordinal numbers. Formalized Mathematics, 1(2):281–290, 1990.

[3] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5):841–845, 1990.

[4] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990.

[5] Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics.

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

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

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

Definition of Convex Function and Jensen’s Inequality

Grigory E. Ivanov Moscow Institute for Physics and Technology

Summary. Convexity of a function in a real linear space is defined as convexity of its epigraph according to “Convex analysis” [24]. The epigraph of a function is a subset of the product of the function’s domain space and the space of real numbers. Therefore, the product of two real linear spaces should be defined. The values of the functions under consideration are extended real numbers. We define the sum of a finite sequence of extended real numbers and get some properties of the sum. The relation between notions “function is convex” and “function is convex on set” (see definition 13 in [21]) is established. We obtain another version of the criterion for a set to be convex (see theorem 6 in [15] to compare) that may be more suitable in some cases. Finally, we prove Jensen’s inequality (both strict and not strict) as criteria for functions to be convex.

MML Identifier: CONVFUN1.

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

1. Product of Two Real Linear Spaces

Let X, Y be non empty RLS structures. The functor AddInProdRLS(X, Y) yielding a binary operation on [: the carrier of X, the carrier of Y :] is defined by the condition (Def. 1).

(Def. 1) Let z_{1}, z_{2} be elements of [: the carrier of X, the carrier of Y :], x_{1}, x_{2} be vectors of X, and y_{1}, y_{2} be vectors of Y. Suppose z_{1} = ⟨⟨x_{1}, y_{1}⟩⟩ and z_{2} = ⟨⟨x_{2}, y_{2}⟩⟩. Then (AddInProdRLS(X, Y))(z_{1}, z_{2}) = ⟨⟨(the addition of X)(⟨⟨x_{1}, x_{2}⟩⟩), (the addition of Y)(⟨⟨y_{1}, y_{2}⟩⟩)⟩⟩.

Let X, Y be non empty RLS structures. The functor MultInProdRLS(X, Y) yields a function from [: ℝ, [: the carrier of X, the carrier of Y :] :] into [: the carrier of X, the carrier of Y :] and is defined by the condition (Def. 2).

(Def. 2) Let a be a real number, z be an element of [: the carrier of X, the carrier of Y :], x be a vector of X, and y be a vector of Y. Suppose z = ⟨⟨x, y⟩⟩. Then (MultInProdRLS(X, Y))(⟨⟨a, z⟩⟩) = ⟨⟨(the external multiplication of X)(⟨⟨a, x⟩⟩), (the external multiplication of Y)(⟨⟨a, y⟩⟩)⟩⟩.

Let X, Y be non empty RLS structures. The functor ProdRLS(X, Y) yields an RLS structure and is defined by:

(Def. 3) ProdRLS(X, Y) = ⟨[: the carrier of X, the carrier of Y :], ⟨⟨0_{X},

0_{Y} ⟩⟩, AddInProdRLS(X, Y), MultInProdRLS(X, Y)⟩. Let X, Y be non empty RLS structures. Note that ProdRLS(X, Y) is non

empty.

Next we state two propositions:

(1) Let X, Y be non empty RLS structures, x be a vector of X, y be a vector of Y, u be a vector of ProdRLS(X, Y), and p be a real number. If u = ⟨⟨x, y⟩⟩, then p · u = ⟨⟨p · x, p · y⟩⟩.

(2) Let X, Y be non empty RLS structures, x_{1}, x_{2} be vectors of X, y_{1}, y_{2} be vectors of Y, and u_{1}, u_{2} be vectors of ProdRLS(X, Y). If u_{1} = ⟨⟨x_{1}, y_{1}⟩⟩ and u_{2} = ⟨⟨x_{2}, y_{2}⟩⟩, then u_{1} + u_{2} = ⟨⟨x_{1} + x_{2}, y_{1} + y_{2}⟩⟩.

Let X, Y be Abelian non empty RLS structures. One can verify that ProdRLS(X, Y) is Abelian.

Let X, Y be add-associative non empty RLS structures. Observe that ProdRLS(X, Y) is add-associative.

Let X, Y be right zeroed non empty RLS structures. Observe that ProdRLS(X, Y) is right zeroed.

Let X, Y be right complementable non empty RLS structures. One can check that ProdRLS(X, Y) is right complementable.

Let X, Y be real linear space-like non empty RLS structures. Observe that ProdRLS(X, Y) is real linear space-like.

Next we state the proposition

(3) Let X, Y be real linear spaces, n be a natural number, x be a finite sequence of elements of the carrier of X, y be a finite sequence of elements of the carrier of Y, and z be a finite sequence of elements of the carrier of ProdRLS(X, Y). Suppose lenx = n and leny = n and lenz = n and for every natural number i such that i ∈ Segn holds z(i) = ⟨⟨x(i), y(i)⟩⟩. Then ∑ z = ⟨⟨∑ x, ∑ y⟩⟩.

2. Real Linear Space of Real Numbers

The non empty RLS structure ℝ_{RLS} is defined as follows: (Def. 4) ℝ_{RLS} = ⟨ℝ, 0, +_{ℝ}, ·_{ℝ}⟩.

Let us note that ℝ_{RLS} is Abelian, add-associative, right zeroed, right complementable, and real linear space-like.

3. Sum of Finite Sequence of Extended Real Numbers

Let F be a finite sequence of elements of \overline{ℝ}. The functor ∑ F yields an extended real number and is defined by the condition (Def. 5).

(Def. 5) There exists a function f from ℕ into \overline{ℝ} such that ∑ F = f(lenF) and f(0) = 0\overline{ℝ} and for every natural number i such that i < lenF holds f(i + 1) = f(i) + F (i + 1).

We now state several propositions:

(4) ∑(ε\overline{ℝ}) = 0\overline{ℝ}.

(5) For every extended real number a holds ∑⟨a⟩ = a.

(6) For all extended real numbers a, b holds ∑⟨a, b⟩ = a + b.

(7) For all finite sequences F, G of elements of \overline{ℝ} such that −∞ ∉ rngF and −∞ ∉ rngG holds ∑(F ^{⌢} G) = ∑ F + ∑ G.

(8) Let F, G be finite sequences of elements of \overline{ℝ} and s be a permutation of domF. If G = F · s and −∞ ∉ rngF, then ∑ F = ∑ G.

4. Definition of Convex Function

Let X be a non empty RLS structure and let f be a function from the carrier of X into \overline{ℝ}. The functor epigraph f yielding a subset of ProdRLS(X, ℝ_{RLS}) is defined as follows:

(Def. 6) epigraphf = {⟨⟨x, y⟩⟩; x ranges over elements of X, y ranges over elements

of ℝ: f(x) \overline{ℝ}(y)\}. Let X be a non empty RLS structure and let f be a function from the carrier

of X into \overline{ℝ}. We say that f is convex if and only if: (Def. 7) epigraph f is convex.

The following two propositions are true:

(9) Let X be a non empty RLS structure and f be a function from the carrier of X into \overline{ℝ}. Suppose that for every vector x of X holds f(x) ≠ −∞. Then f is convex if and only if for all vectors x_{1}, x_{2} of X and for every real number p such that 0 < p and p < 1 holds f(p · x_{1} + (1 − p) · x_{2}) \overline{ℝ}(p) · f(x_{1}) + \overline{ℝ}(1 − p) · f(x_{2}).

(10) Let X be a real linear space and f be a function from the carrier of X into \overline{ℝ}. Suppose that for every vector x of X holds f(x) ≠ −∞. Then f is convex if and only if for all vectors x_{1}, x_{2} of X and for every real number p such that 0 p and p 1 holds f(p · x_{1} + (1 − p) · x_{2}) \overline{ℝ}(p) · f(x_{1}) + \overline{ℝ}(1 − p) · f(x_{2}).

5. Relation between Notions “function is convex” and “function is convex on set”

We now state the proposition

(11) Let f be a partial function from ℝ to ℝ, g be a function from the carrier of ℝ_{RLS} into \overline{ℝ}, and X be a subset of ℝ_{RLS}. Suppose X ⊆ domf and for every real number x holds if x ∈ X, then g(x) = f(x) and if x ∉ X, then g(x) = +∞. Then g is convex if and only if the following conditions are satisfied:

(i) f is convex on X, and (ii) X is convex.

6. Theorem 6 from [15] in Other Words

One can prove the following proposition

(12) Let X be a real linear space and M be a subset of X. Then M is convex if and only if for every non empty natural number n and for every finite sequence p of elements of ℝ and for all finite sequences y, z of elements of the carrier of X such that lenp = n and leny = n and lenz = n and ∑ p = 1 and for every natural number i such that i ∈ Segn holds p(i) > 0 and z(i) = p(i) · y_{i} and y_{i} ∈ M holds ∑ z ∈ M.

7. Jensen’s Inequality

One can prove the following two propositions:

(13) Let X be a real linear space and f be a function from the carrier of X into \overline{ℝ}. Suppose that for every vector x of X holds f(x) ≠ −∞. Then f is convex if and only if for every non empty natural number n and for every finite sequence p of elements of ℝ and for every finite sequence F of elements of \overline{ℝ} and for all finite sequences y, z of elements of the carrier of X such that lenp = n and lenF = n and leny = n and lenz = n and ∑ p = 1 and for every natural number i such that i ∈ Segn holds p(i) > 0 and z(i) = p(i) · y_{i} and F (i) = \overline{ℝ}(p(i)) · f(y_{i}) holds f(∑ z) ∑ F.

definition of convex function … 353

(14) Let X be a real linear space and f be a function from the carrier of X into \overline{ℝ}. Suppose that for every vector x of X holds f(x) ≠ −∞. Then f is convex if and only if for every non empty natural number n and for every finite sequence p of elements of ℝ and for every finite sequence F of elements of \overline{ℝ} and for all finite sequences y, z of elements of the carrier of X such that lenp = n and lenF = n and leny = n and lenz = n and ∑ p = 1 and for every natural number i such that i ∈ Segn holds p(i) 0 and z(i) = p(i) · y_{i} and F (i) = \overline{ℝ}(p(i)) · f(y_{i}) holds f(∑ z) ∑ F.

Acknowledgments

I thank Andrzej Trybulec for teaching me Mizar.

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] Józef Białas. Infimum and supremum of the set of real numbers. Measure theory. Formalized Mathematics, 2(1):163–171, 1991.

[5] Józef Białas. Series of positive real numbers. Measure theory. Formalized Mathematics, 2(1):173–183, 1991.

[6] Józef Białas. Some properties of the intervals. Formalized Mathematics, 5(1):21–26, 1996.

[7] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 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. Partial functions. Formalized Mathematics, 1(2):357–367, 1990.

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

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

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

[14] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Convex sets and convex combinations. Formalized Mathematics, 11(1):53–58, 2003.

[15] Noboru Endou, Yasumasa Suzuki, and Yasunari Shidama. Some properties for convex combinations. Formalized Mathematics, 11(3):267–270, 2003.

[16] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Basic properties of extended real numbers. Formalized Mathematics, 9(3):491–494, 2001.

[17] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Definitions and basic properties of measurable functions. Formalized Mathematics, 9(3):495–500, 2001.

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

[19] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269–272, 1990.

[20] Jarosław Kotowicz. Functions and finite sequences of real numbers. Formalized Mathematics, 3(2):275–278, 1992.

[21] Jarosław Kotowicz and Yuji Sakai. Properties of partial functions from a domain to the set of real numbers. Formalized Mathematics, 3(2):279–288, 1992.

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

354 grigory e. ivanov

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

[24] Tyrrell R. Rockafellar. Convex Analysis. Princeton University Press, 1970.

[25] Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics.

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

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

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

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

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

[31] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.

Received July 17, 2003

On Semilattice Structure of Mizar Types

Grzegorz Bancerek Białystok Technical University

Summary. The aim of this paper is to develop a formal theory of Mizar types. The presented theory is an approach to the structure of Mizar types as a sup-semilattice with widening (subtyping) relation as the order. It is an abstraction from the existing implementation of the Mizar verifier and formalization of the ideas from [9].

MML Identifier: ABCMIZ 0.

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

1. Semilattice of Widening

Let us mention that every non empty relational structure which is trivial and reflexive is also complete.

Let T be a relational structure. A type of T is an element of T.

Let T be a relational structure. We say that T is Noetherian if and only if: (Def. 1) The internal relation of T is reversely well founded.

Let us observe that every non empty relational structure which is trivial is also Noetherian.

Let T be a non empty relational structure. Let us observe that T is Noetherian if and only if the condition (Def. 2) is satisfied.

(Def. 2) Let A be a non empty subset of T. Then there exists an element a of T

such that a ∈ A and for every element b of T such that b ∈ A holds a ≮ b. Let T be a poset. We say that T is Mizar-widening-like if and only if:

(Def. 3) T is a sup-semilattice and Noetherian.

Let us mention that every poset which is Mizar-widening-like is also Noetherian and upper-bounded and has l.u.b.’s.

Let us note that every sup-semilattice which is Noetherian is also Mizarwidening-like.

Let us observe that there exists a complete sup-semilattice which is Mizarwidening-like.

Let T be a Noetherian relational structure. One can check that the internal relation of T is reversely well founded.

Next we state the proposition

(1) For every Noetherian sup-semilattice T and for every ideal I of T holds sup I exists in T and supI ∈ I.

2. Adjectives

We consider adjective structures as systems ⟨ a set of adjectives, an operation non ⟩,

where the set of adjectives is a set and the operation non is a unary operation on the set of adjectives.

Let A be an adjective structure. We say that A is void if and only if: (Def. 4) The set of adjectives of A is empty.

An adjective of A is an element of the set of adjectives of A.

The following proposition is true

(2) Let A_{1}, A_{2} be adjective structures. Suppose the set of adjectives of A_{1} = the set of adjectives of A_{2}. If A_{1} is void, then A_{2} is void.

Let A be an adjective structure and let a be an element of the set of adjectives of A. The functor nona yields an adjective of A and is defined as follows:

(Def. 5) nona = (the operation non of A)(a).

One can prove the following proposition

(3) Let A_{1}, A_{2} be adjective structures. Suppose the adjective structure of A_{1} = the adjective structure of A_{2}. Let a_{1} be an adjective of A_{1} and a_{2} be an adjective of A_{2}. If a_{1} = a_{2}, then nona_{1} = nona_{2}.

Let A be an adjective structure. We say that A is involutive if and only if: (Def. 6) For every adjective a of A holds nonnona = a.

We say that A is without fixpoints if and only if: (Def. 7) It is not true that there exists an adjective a of A such that nona = a.

We now state three propositions:

(4) Let a_{1}, a_{2} be sets. Suppose a_{1} ≠ a_{2}. Let A be an adjective structure. Suppose the set of adjectives of A = {a_{1}, a_{2}} and (the operation non of A)(a_{1}) = a_{2} and (the operation non of A)(a_{2}) = a_{1}. Then A is non void, involutive, and without fixpoints.

(5) Let A_{1}, A_{2} be adjective structures. Suppose the adjective structure of A_{1} = the adjective structure of A_{2}. If A_{1} is involutive, then A_{2} is involutive.

(6) Let A_{1}, A_{2} be adjective structures. Suppose the adjective structure of A_{1} = the adjective structure of A_{2}. If A_{1} is without fixpoints, then A_{2} is without fixpoints.

Let us observe that there exists a strict adjective structure which is non void, involutive, and without fixpoints.

Let A be a non void adjective structure. Observe that the set of adjectives of A is non empty.

We consider TA-structures as extensions of relational structure and adjective structure as systems

⟨ a carrier, a set of adjectives, an internal relation, an operation non, an adjective map ⟩, where the carrier and the set of adjectives are sets, the internal relation is a binary relation on the carrier, the operation non is a unary operation on the set of adjectives, and the adjective map is a function from the carrier into Finthe set of adjectives.

Let X be a non empty set, let A be a set, let r be a binary relation on X, let n be a unary operation on A, and let a be a function from X into FinA. Observe that ⟨X, A, r, n, a⟩ is non empty.

Let X be a set, let A be a non empty set, let r be a binary relation on X, let n be a unary operation on A, and let a be a function from X into FinA. One can check that ⟨X, A, r, n, a⟩ is non void.

One can check that there exists a TA-structure which is trivial, reflexive, non empty, non void, involutive, without fixpoints, and strict.

Let T be a TA-structure and let t be an element of T. The functor adjst yields a subset of the set of adjectives of T and is defined as follows:

(Def. 8) adjst = (the adjective map of T)(t).

One can prove the following proposition

(7) Let T_{1}, T_{2} be TA-structures. Suppose the TA-structure of T_{1} = the TAstructure of T_{2}. Let t_{1} be a type of T_{1} and t_{2} be a type of T_{2}. If t_{1} = t_{2}, then adjst_{1} = adjst_{2}.

Let T be a TA-structure. We say that T is consistent if and only if:

(Def. 9) For every type t of T and for every adjective a of T such that a ∈ adjst

holds nona ∉ adjst. Next we state the proposition

(8) Let T_{1}, T_{2} be TA-structures. Suppose the TA-structure of T_{1} = the TAstructure of T_{2}. If T_{1} is consistent, then T_{2} is consistent.

Let T be a non empty TA-structure. We say that T has structured adjectives if and only if:

(Def. 10) The adjective map of T is a join-preserving map from T into

(2_{⊆}^{the set of adjectives of T})^{op}. We now state the proposition

(9) Let T_{1}, T_{2} be non empty TA-structures. Suppose the TA-structure of T_{1} = the TA-structure of T_{2}. If T_{1} has structured adjectives, then T_{2} has structured adjectives.

Let T be a reflexive transitive antisymmetric TA-structure with l.u.b.’s. Let us observe that T has structured adjectives if and only if:

(Def. 11) For all types t_{1}, t_{2} of T holds adjs(t_{1} ⊔ t_{2}) = adjst_{1} ∩ adjst_{2}.

One can prove the following proposition

(10) Let T be a reflexive transitive antisymmetric TA-structure with l.u.b.’s. Suppose T has structured adjectives. Let t_{1}, t_{2} be types of T. If t_{1} t_{2}, then adjst_{2} ⊆ adjst_{1}.

Let T be a TA-structure and let a be an element of the set of adjectives of T. The functor typesa yields a subset of T and is defined as follows:

(Def. 12) For every set x holds x ∈ typesa iff there exists a type t of T such that

x = t and a ∈ adjst. Let T be a non empty TA-structure and let A be a subset of the set of

adjectives of T. The functor typesA yielding a subset of T is defined as follows: (Def. 13) For every type t of T holds t ∈ typesA iff for every adjective a of T such

that a ∈ A holds t ∈ typesa. One can prove the following propositions:

(11) Let T_{1}, T_{2} be TA-structures. Suppose the TA-structure of T_{1} = the TAstructure of T_{2}. Let a_{1} be an adjective of T_{1} and a_{2} be an adjective of T_{2}. If a_{1} = a_{2}, then typesa_{1} = typesa_{2}.

(12) For every non empty TA-structure T and for every adjective a of T holds typesa = {t; t ranges over types of T: a ∈ adjst}.

(13) Let T be a TA-structure, t be a type of T, and a be an adjective of T. Then a ∈ adjst if and only if t ∈ typesa.

(14) Let T be a non empty TA-structure, t be a type of T, and A be a subset of the set of adjectives of T. Then A ⊆ adjst if and only if t ∈ typesA.

(15) For every non void TA-structure T and for every type t of T holds adjst = {a; a ranges over adjectives of T: t ∈ typesa}.

(16) Let T be a non empty TA-structure and t be a type of T. Then

types(∅_{the set of adjectives of T}) = the carrier of T. Let T be a TA-structure. We say that T has typed adjectives if and only if:

(Def. 14) For every adjective a of T holds typesa ∪ typesnona is non empty.

We now state the proposition

(17) Let T_{1}, T_{2} be TA-structures. Suppose the TA-structure of T_{1} = the TA-

structure of T_{2}. If T_{1} has typed adjectives, then T_{2} has typed adjectives. Let us mention that there exists a complete upper-bounded non empty trivial

reflexive transitive antisymmetric strict TA-structure which is non void, Mizarwidening-like, involutive, without fixpoints, and consistent and has structured adjectives and typed adjectives.

Next we state the proposition

(18) For every consistent TA-structure T and for every adjective a of T holds

typesa misses typesnona. Let T be a reflexive transitive antisymmetric TA-structure with l.u.b.’s with

structured adjectives and let a be an adjective of T. Note that typesa is lower and directed.

Let T be a reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives and let A be a subset of the set of adjectives of T. One can verify that typesA is lower and directed.

We now state the proposition

(19) Let T be reflexive antisymmetric transitive TA-structure with l.u.b.’s with structured adjectives and a be an adjective of T. Then typesa is empty or typesa is an ideal of T.

3. Applicability of Adjectives

Let T be a TA-structure, let t be an element of T, and let a be an adjective of T. We say that a is applicable to t if and only if:

(Def. 15) There exists a type t′ of T such that t′∈ typesa and t′ t.

Let T be a TA-structure, let t be a type of T, and let A be a subset of the set of adjectives of T. We say that A is applicable to t if and only if:

(Def. 16) There exists a type t′ of T such that A ⊆ adjst′ and t′ t.

We now state the proposition

(20) Let T be a reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, a be an adjective of T, and t be a type of T. If a is applicable to t, then typesa ∩ ↓t is an ideal of T.

Let T be a non empty reflexive transitive TA-structure, let t be an element of T, and let a be an adjective of T. The functor a ∗ t yielding a type of T is defined by:

(Def. 17) a ∗ t = sup(typesa ∩ ↓t).

The following propositions are true:

(21) Let T be a Noetherian reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, t be a type of T, and a be an adjective of T. If a is applicable to t, then a ∗ t t.

(22) Let T be a Noetherian reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, t be a type of T, and a be an adjective of T. If a is applicable to t, then a ∈ adjs(a ∗ t).

(23) Let T be a Noetherian reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, t be a type of T, and a be an adjective of T. If a is applicable to t, then a ∗ t ∈ typesa.

(24) Let T be a Noetherian reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, t be a type of T, a be an adjective of T, and t′ be a type of T. If t′ t and a ∈ adjst′, then a is applicable to t and t′ a ∗ t.

(25) Let T be a Noetherian reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, t be a type of T, and a be an adjective of T. If a ∈ adjst, then a is applicable to t and a ∗ t = t.

(26) Let T be a Noetherian reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, t be a type of T, and a, b be adjectives of T. Suppose a is applicable to t and b is applicable to a ∗ t. Then b is applicable to t and a is applicable to b∗t and a∗(b∗t) = b∗(a∗t).

(27) Let T be a reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, A be a subset of the set of adjectives of T, and t be a type of T. If A is applicable to t, then typesA ∩ ↓t is an ideal of T.

Let T be a non empty reflexive transitive TA-structure, let t be a type of T, and let A be a subset of the set of adjectives of T. The functor A ∗ t yielding a type of T is defined as follows:

(Def. 18) A ∗ t = sup(typesA ∩ ↓t).

Next we state the proposition

(28) Let T be a non empty reflexive transitive antisymmetric TA-structure and t be a type of T. Then ∅_{the set of adjectives of T} ∗ t = t.

Let T be a non empty non void reflexive transitive TA-structure, let t be a type of T, and let p be a finite sequence of elements of the set of adjectives of T. The functor apply(p, t) yielding a finite sequence of elements of the carrier of T is defined by the conditions (Def. 19).

(Def. 19)(i) lenapply(p, t) = lenp + 1, (ii) (apply(p, t))(1) = t, and (iii) for every natural number i and for every adjective a of T and for every

type t of T such that i ∈ domp and a = p(i) and t = (apply(p, t))(i) holds (apply(p, t))(i + 1) = a ∗ t.

Let T be a non empty non void reflexive transitive TA-structure, let t be a type of T, and let p be a finite sequence of elements of the set of adjectives of T. Note that apply(p, t) is non empty.

One can prove the following two propositions:

(29) Let T be a non empty non void reflexive transitive TA-structure and t be a type of T. Then apply(ε_{(the set of adjectives of T)}, t) = ⟨t⟩.

(30) Let T be a non empty non void reflexive transitive TA-structure, t be a

type of T, and a be an adjective of T. Then apply(⟨a⟩, t) = ⟨t, a ∗ t⟩. Let T be a non empty non void reflexive transitive TA-structure, let t be a

type of T, and let v be a finite sequence of elements of the set of adjectives of T. The functor v ∗ t yielding a type of T is defined by:

(Def. 20) v ∗ t = (apply(v, t))(lenv + 1).

The following propositions are true:

(31) Let T be a non empty non void reflexive transitive TA-structure and t be a type of T. Then ε_{(the set of adjectives of T)} ∗ t = t.

(32) Let T be a non empty non void reflexive transitive TA-structure, t be a type of T, and a be an adjective of T. Then ⟨a⟩ ∗ t = a ∗ t.

(33) For all finite sequences p, q and for every natural number i such that i 1 and i < lenp holds (p^{$⌢} q)(i) = p(i).

(34) Let p be a non empty finite sequence, q be a finite sequence, and i be a natural number. If i < lenq, then (p^{$⌢} q)(lenp + i) = q(i + 1).

(35) Let T be a non empty non void reflexive transitive TA-structure, t be a type of T, and v_{1}, v_{2} be finite sequences of elements of the set of adjectives of T. Then apply(v_{1} ^{⌢} v_{2}, t) = (apply(v_{1}, t))^{$⌢} apply(v_{2}, v_{1} ∗ t).

(36) Let T be a non empty non void reflexive transitive TA-structure, t be a type of T, v_{1}, v_{2} be finite sequences of elements of the set of adjectives of T, and i be a natural number. If i ∈ domv_{1}, then (apply(v_{1} ^{⌢} v_{2}, t))(i) = (apply(v_{1}, t))(i).

(37) Let T be a non empty non void reflexive transitive TA-structure, t be a type of T, and v_{1}, v_{2} be finite sequences of elements of the set of adjectives of T. Then (apply(v_{1} ^{⌢} v_{2}, t))(lenv_{1} + 1) = v_{1} ∗ t.

(38) Let T be a non empty non void reflexive transitive TA-structure, t be a type of T, and v_{1}, v_{2} be finite sequences of elements of the set of adjectives of T. Then v_{2} ∗ (v_{1} ∗ t) = (v_{1} ^{⌢} v_{2}) ∗ t.

Let T be a non empty non void reflexive transitive TA-structure, let t be a type of T, and let v be a finite sequence of elements of the set of adjectives of T. We say that v is applicable to t if and only if the condition (Def. 21) is satisfied.

(Def. 21) Let i be a natural number, a be an adjective of T, and s be a type of T. If i ∈ domv and a = v(i) and s = (apply(v, t))(i), then a is applicable to s.

Next we state a number of propositions:

(39) Let T be a non empty non void reflexive transitive TA-structure and t be a type of T. Then ε_{(the set of adjectives of T)} is applicable to t.

(40) Let T be a non empty non void reflexive transitive TA-structure, t be a type of T, and a be an adjective of T. Then a is applicable to t if and only if ⟨a⟩ is applicable to t.

(41) Let T be a non empty non void reflexive transitive TA-structure, t be a type of T, and v_{1}, v_{2} be finite sequences of elements of the set of adjectives of T. Suppose v_{1} ^{⌢} v_{2} is applicable to t. Then v_{1} is applicable to t and v_{2} is applicable to v_{1} ∗ t.

(42) Let T be a Noetherian reflexive transitive antisymmetric non void TAstructure with l.u.b.’s with structured adjectives, t be a type of T, and v be a finite sequence of elements of the set of adjectives of T. Suppose v is applicable to t. Let i_{1}, i_{2} be natural numbers. Suppose 1 i_{1} and i_{1} i_{2} and i_{2} lenv + 1. Let t_{1}, t_{2} be types of T. If t_{1} = (apply(v, t))(i_{1}) and t_{2} = (apply(v, t))(i_{2}), then t_{2} t_{1}.

(43) Let T be a Noetherian reflexive transitive antisymmetric non void TAstructure with l.u.b.’s with structured adjectives, t be a type of T, and v be a finite sequence of elements of the set of adjectives of T. Suppose v is applicable to t. Let s be a type of T. If s ∈ rngapply(v, t), then v ∗ t s and s t.

(44) Let T be a Noetherian reflexive transitive antisymmetric non void TAstructure with l.u.b.’s with structured adjectives, t be a type of T, and v be a finite sequence of elements of the set of adjectives of T. If v is applicable to t, then v ∗ t t.

(45) Let T be a Noetherian reflexive transitive antisymmetric non void TAstructure with l.u.b.’s with structured adjectives, t be a type of T, and v be a finite sequence of elements of the set of adjectives of T. If v is applicable to t, then rngv ⊆ adjs(v ∗ t).

(46) Let T be a Noetherian reflexive transitive antisymmetric non void TAstructure with l.u.b.’s with structured adjectives, t be a type of T, and v be a finite sequence of elements of the set of adjectives of T. Suppose v is applicable to t. Let A be a subset of the set of adjectives of T. If A = rngv, then A is applicable to t.

(47) Let T be a Noetherian reflexive transitive antisymmetric non void TAstructure with l.u.b.’s with structured adjectives, t be a type of T, and v_{1}, v_{2} be finite sequences of elements of the set of adjectives of T. Suppose v_{1} is applicable to t and rngv_{2} ⊆ rngv_{1}. Let s be a type of T. If s ∈ rngapply(v_{2}, t), then v_{1} ∗ t s.

(48) Let T be a Noetherian reflexive transitive antisymmetric non void TAstructure with l.u.b.’s with structured adjectives, t be a type of T, and v_{1}, v_{2} be finite sequences of elements of the set of adjectives of T. If v_{1} ^{⌢} v_{2} is applicable to t, then v_{2} ^{⌢} v_{1} is applicable to t.

(49) Let T be a Noetherian reflexive transitive antisymmetric non void TAstructure with l.u.b.’s with structured adjectives, t be a type of T, and v_{1}, v_{2} be finite sequences of elements of the set of adjectives of T. If v_{1} ^{⌢} v_{2} is applicable to t, then (v_{1} ^{⌢} v_{2}) ∗ t = (v_{2} ^{⌢} v_{1}) ∗ t.

(50) Let T be a Noetherian reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, t be a type of T, and A be a subset of the set of adjectives of T. If A is applicable to t, then A ∗ t t.

(51) Let T be a Noetherian reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, t be a type of T, and A be a subset of the set of adjectives of T. If A is applicable to t, then A ⊆ adjs(A ∗ t).

(52) Let T be a Noetherian reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, t be a type of T, and A be a subset of the set of adjectives of T. If A is applicable to t, then A ∗ t ∈ typesA.

(53) Let T be a Noetherian reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, t be a type of T, A be a subset of the set of adjectives of T, and t′ be a type of T. If t′ t and A ⊆ adjst′, then A is applicable to t and t′ A ∗ t.

(54) Let T be a Noetherian reflexive transitive antisymmetric TA-structure with l.u.b.’s with structured adjectives, t be a type of T, and A be a subset of the set of adjectives of T. If A ⊆ adjst, then A is applicable to t and A ∗ t = t.

(55) Let T be a TA-structure, t be a type of T, and A, B be subsets of the set of adjectives of T. If A is applicable to t and B ⊆ A, then B is applicable to t.

(56) Let T be a Noetherian reflexive transitive antisymmetric non void TAstructure with l.u.b.’s with structured adjectives, t be a type of T, a be an adjective of T, and A, B be subsets of the set of adjectives of T. If B = A ∪ {a} and B is applicable to t, then a ∗ (A ∗ t) = B ∗ t.

(57) Let T be a Noetherian reflexive transitive antisymmetric non void TAstructure with l.u.b.’s with structured adjectives, t be a type of T, and v be a finite sequence of elements of the set of adjectives of T. Suppose v is applicable to t. Let A be a subset of the set of adjectives of T. If A = rngv, then v ∗ t = A ∗ t.

4. Subject Function

Let T be a non empty non void TA-structure. The functor subT yields a function from the set of adjectives of T into the carrier of T and is defined as follows:

(Def. 22) For every adjective a of T holds (subT)(a) = sup(typesa ∪ typesnona).

We introduce TAS-structures which are extensions of TA-structure and are systems

⟨ a carrier, a set of adjectives, an internal relation, an operation non, an adjective map, a subject map ⟩, where the carrier and the set of adjectives are sets, the internal relation is a binary relation on the carrier, the operation non is a unary operation on the set of adjectives, the adjective map is a function from the carrier into Finthe set of adjectives, and the subject map is a function from the set of adjectives into the carrier.

Let us observe that there exists a TAS-structure which is non void, reflexive, trivial, non empty, and strict.

Let T be a non empty non void TAS-structure and let a be an adjective of T. The functor suba yields a type of T and is defined as follows:

(Def. 23) suba = (the subject map of T)(a).

Let T be a non empty non void TAS-structure. We say that T is absorbing non if and only if:

(Def. 24) (The subject map of T) · (the operation non of T) = the subject map of

T. We say that T is subjected if and only if:

(Def. 25) For every adjective a of T holds typesa ∪ typesnona suba and if

typesa ≠ ∅ and typesnona ≠ ∅, then suba = sup(typesa ∪ typesnona). Let T be a non empty non void TAS-structure. Let us observe that T is

absorbing non if and only if: (Def. 26) For every adjective a of T holds subnona = suba.

Let T be a non empty non void TAS-structure, let t be an element of T, and let a be an adjective of T. We say that a is properly applicable to t if and only if:

(Def. 27) t suba and a is applicable to t.

Let T be a non empty non void reflexive transitive TAS-structure, let t be a type of T, and let v be a finite sequence of elements of the set of adjectives of T. We say that v is properly applicable to t if and only if the condition (Def. 28) is satisfied.

(Def. 28) Let i be a natural number, a be an adjective of T, and s be a type of T. If i ∈ domv and a = v(i) and s = (apply(v, t))(i), then a is properly

applicable to s. One can prove the following propositions:

(58) Let T be a non empty non void reflexive transitive TAS-structure, t be a type of T, and v be a finite sequence of elements of the set of adjectives of T. If v is properly applicable to t, then v is applicable to t.

(59) Let T be a non empty non void reflexive transitive TAS-structure and t be a type of T. Then ε_{(the set of adjectives of T)} is properly applicable to t.

(60) Let T be a non empty non void reflexive transitive TAS-structure, t be a type of T, and a be an adjective of T. Then a is properly applicable to t if and only if ⟨a⟩ is properly applicable to t.

(61) Let T be a non empty non void reflexive transitive TAS-structure, t be a type of T, and v_{1}, v_{2} be finite sequences of elements of the set of adjectives of T. Suppose v_{1} ^{⌢} v_{2} is properly applicable to t. Then v_{1} is properly applicable to t and v_{2} is properly applicable to v_{1} ∗ t.

(62) Let T be a non empty non void reflexive transitive TAS-structure, t be a type of T, and v_{1}, v_{2} be finite sequences of elements of the set of adjectives of T. Suppose v_{1} is properly applicable to t and v_{2} is properly applicable to v_{1} ∗ t. Then v_{1} ^{⌢} v_{2} is properly applicable to t.

Let T be a non empty non void reflexive transitive TAS-structure, let t be a type of T, and let A be a subset of the set of adjectives of T. We say that A is properly applicable to t if and only if the condition (Def. 29) is satisfied.

(Def. 29) There exists a finite sequence s of elements of the set of adjectives of T

such that rngs = A and s is properly applicable to t. Next we state two propositions:

(63) Let T be a non empty non void reflexive transitive TAS-structure, t be a type of T, and A be a subset of the set of adjectives of T. If A is properly applicable to t, then A is finite.

(64) Let T be a non empty non void reflexive transitive TAS-structure and t

be a type of T. Then ∅_{the set of adjectives of T} is properly applicable to t. The scheme MinimalFiniteSet concerns a unary predicate P, and states that:

There exists a finite set A such that P[A] and for every set B such that B ⊆ A and P[B] holds B = A

provided the following requirement is met:

• There exists a finite set A such that P[A]. One can prove the following proposition

(65) Let T be a non empty non void reflexive transitive TAS-structure, t be a type of T, and A be a subset of the set of adjectives of T. Suppose A is properly applicable to t. Then there exists a subset B of the set of adjectives of T such that

(i) B ⊆ A, (ii) B is properly applicable to t, (iii) A ∗ t = B ∗ t, and (iv) for every subset C of the set of adjectives of T such that C ⊆ B and C

is properly applicable to t and A ∗ t = C ∗ t holds C = B. Let T be a non empty non void reflexive transitive TAS-structure. We say

that T is commutative if and only if the condition (Def. 30) is satisfied. (Def. 30) Let t_{1}, t_{2} be types of T and a be an adjective of T. Suppose a is properly

applicable to t_{1} and a ∗ t_{1} t_{2}. Then there exists a finite subset A of the set of adjectives of T such that A is properly applicable to t_{1} ⊔ t_{2} and A ∗ (t_{1} ⊔ t_{2}) = t_{2}.

Let us observe that there exists a complete upper-bounded non empty non void trivial reflexive transitive antisymmetric strict TAS-structure which is Mizar-widening-like, involutive, without fixpoints, consistent, absorbing non, subjected, and commutative and has structured adjectives and typed adjectives.

Next we state the proposition

(66) Let T be a Noetherian reflexive transitive antisymmetric non void TASstructure with l.u.b.’s with structured adjectives, t be a type of T, and A be a subset of the set of adjectives of T. Suppose A is properly applicable to t. Then there exists an one-to-one finite sequence s of elements of the set of adjectives of T such that rngs = A and s is properly applicable to t.

5. Reduction of Adjectives

Let T be a non empty non void reflexive transitive TAS-structure. The functor \underrightarrow{∘} _{T} yields a binary relation on T and is defined by the condition (Def. 31).

(Def. 31) Let t_{1}, t_{2} be types of T. Then ⟨⟨t_{1}, t_{2}⟩⟩∈ \underrightarrow{∘} _{T} if and only if there exists an adjective a of T such that a ∉ adjst_{2} and a is properly applicable to t_{2} and a ∗ t_{2} = t_{1}.

Next we state the proposition

(67) Let T be an antisymmetric non void reflexive transitive Noetherian TASstructure with l.u.b.’s with structured adjectives. Then \underrightarrow{∘} _{T} ⊆ the internal relation of T.

The scheme RedInd deals with a non empty set A, a binary relation B on A, and a binary predicate P, and states that:

For all elements x, y of A such that B reduces x to y holds P[x, y] provided the parameters have the following properties:

• For all elements x, y of A such that ⟨⟨x, y⟩⟩∈ B holds P[x, y],

• For every element x of A holds P[x, x], and

• For all elements x, y, z of A such that P[x, y] and P[y, z] holds P[x, z].

We now state a number of propositions:

(68) Let T be an antisymmetric non void reflexive transitive Noetherian TASstructure with l.u.b.’s with structured adjectives and t_{1}, t_{2} be types of T. If \underrightarrow{∘} _{T} reduces t_{1} to t_{2}, then t_{1} t_{2}.

(69) Let T be a Noetherian reflexive transitive antisymmetric non void TASstructure with l.u.b.’s with structured adjectives. Then \underrightarrow{∘} _{T} is irreflexive.

(70) Let T be an antisymmetric non void reflexive transitive Noetherian TASstructure with l.u.b.’s with structured adjectives. Then \underrightarrow{∘} _{T} is stronglynormalizing.

(71) Let T be a Noetherian reflexive transitive antisymmetric non void TASstructure with l.u.b.’s with structured adjectives, t be a type of T, and A be a finite subset of the set of adjectives of T. Suppose that for every subset C of the set of adjectives of T such that C ⊆ A and C is properly applicable to t and A ∗ t = C ∗ t holds C = A. Let s be an one-to-one finite sequence of elements of the set of adjectives of T. Suppose rngs = A and s is properly applicable to t. Let i be a natural number. If 1 i and i lens, then ⟨⟨(apply(s, t))(i + 1), (apply(s, t))(i)⟩⟩∈ \underrightarrow{∘} _{T} .

(72) Let T be a Noetherian reflexive transitive antisymmetric non void TASstructure with l.u.b.’s with structured adjectives, t be a type of T, and A be a finite subset of the set of adjectives of T. Suppose that for every subset C of the set of adjectives of T such that C ⊆ A and C is properly applicable to t and A∗t = C ∗t holds C = A. Let s be an one-to-one finite sequence of elements of the set of adjectives of T. Suppose rngs = A and s is properly applicable to t. Then Rev(apply(s, t)) is a reduction sequence w.r.t. \underrightarrow{∘} _{T}.

(73) Let T be a Noetherian reflexive transitive antisymmetric non void TASstructure with l.u.b.’s with structured adjectives, t be a type of T, and A be a finite subset of the set of adjectives of T. If A is properly applicable to t, then \underrightarrow{∘} _{T} reduces A ∗ t to t.

(74) Let X be a non empty set, R be a binary relation on X, and r be a reduction sequence w.r.t. R. If r(1) ∈ X, then r is a finite sequence of elements of X.

(75) Let X be a non empty set, R be a binary relation on X, x be an element of X, and y be a set. If R reduces x to y, then y ∈ X.

(76) Let X be a non empty set and R be a binary relation on X. Suppose R is weakly-normalizing and has unique normal form property. Let x be an element of X. Then nf_{R}(x) ∈ X.

(77) Let T be a Noetherian reflexive transitive antisymmetric non void TASstructure with l.u.b.’s with structured adjectives and t_{1}, t_{2} be types of T. Suppose \underrightarrow{∘} _{T} reduces t_{1} to t_{2}. Then there exists a finite subset A of the set

of adjectives of T such that A is properly applicable to t_{2} and t_{1} = A ∗ t_{2}.

(78) Let T be an antisymmetric commutative non void reflexive transitive Noetherian TAS-structure with l.u.b.’s with structured adjectives. Then \underrightarrow{∘} _{T} has Church-Rosser property and unique normal form property.

6. Radix Types

Let T be an antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure with structured adjectives and l.u.b.’s and let t be a type of T. The functor radixt yielding a type of T is defined by:

(Def. 32) radixt = nf_{\underrightarrow{∘} _{T}} (t).

We now state several propositions:

(79) Let T be an antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure with structured adjectives and l.u.b.’s and t be a type of T. Then \underrightarrow{∘} _{T} reduces t to radixt.

(80) Let T be an antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure with structured adjectives and l.u.b.’s and t be a type of T. Then t radixt.

(81) Let T be an antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure with structured adjectives and l.u.b.’s, t be a type of T, and X be a set. Suppose X = {t′; t′ ranges over types of T: ⋁_{A: finite subset of the set of adjectives of T} (A is properly applicable to t′ ∧ A ∗ t′= t)}. Then sup X exists in T and radixt = ⨆_{T} X.

(82) Let T be an antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure with structured adjectives and l.u.b.’s, t_{1}, t_{2} be types of T, and a be an adjective of T. If a is properly applicable to t_{1} and a ∗ t_{1} radixt_{2}, then t_{1} radixt_{2}.

(83) Let T be an antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure with structured adjectives and l.u.b.’s and t_{1}, t_{2} be types of T. If t_{1} t_{2}, then radixt_{1} radixt_{2}.

(84) Let T be an antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure with structured adjectives and l.u.b.’s, t be a type of T, and a be an adjective of T. If a is properly applicable to t, then radix(a ∗ t) = radixt.

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. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.

on semilattice structure of mizar types 369

[4] Grzegorz Bancerek. Sequences of ordinal numbers. Formalized Mathematics, 1(2):281– 290, 1990.

[5] Grzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719–725, 1991.

[6] Grzegorz Bancerek. Reduction relations. Formalized Mathematics, 5(4):469–478, 1996.

[7] Grzegorz Bancerek. Bounds in posets and relational substructures. Formalized Mathematics, 6(1):81–91, 1997.

[8] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93–107, 1997.

[9] Grzegorz Bancerek. On the structure of Mizar types. In Herman Geuvers and Fairouz Kamareddine, editors, Electronic Notes in Theoretical Computer Science, volume 85. Elsevier, 2003.

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

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

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

[13] Czesław Byliński. The modification of a function by a function and the iteration of the composition of a function. Formalized Mathematics, 1(3):521–527, 1990.

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

[15] Czesław Byliński. Some properties of restrictions of finite sequences. Formalized Mathematics, 5(2):241–245, 1996.

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

[17] Adam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Formalized Mathematics, 6(1):117–121, 1997.

[18] Małgorzata Korolkiewicz. Homomorphisms of algebras. Quotient universal algebra. Formalized Mathematics, 4(1):109–113, 1993.

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

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

[21] Andrzej Trybulec and Agata Darmochwał. Boolean domains. Formalized Mathematics, 1(1):187–190, 1990.

[22] Wojciech A. Trybulec. Partially ordered sets. Formalized Mathematics, 1(2):313–319, 1990.

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

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

[25] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.

[26] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Formalized Mathematics, 1(1):85–89, 1990.

Lines in n-Dimensional Euclidean Spaces

Akihiro Kubo Shinshu University Nagano

Summary. In this paper, we define the line of n-dimensional Euclidean space and we introduce basic properties of affine space on this space. Next, we define the inner product of elements of this space. At the end, we introduce orthogonality of lines of this space.

MML Identifier: EUCLID 4.

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

We adopt the following rules: a, b, l_{1} are real numbers, n is a natural number, and x, x_{1}, x_{2}, y_{1}, y_{2} are elements of R^{n}.

Next we state several propositions:

(1) 0 · x + x = x and x + ⟨\underbrace{0, …, 0}_{n}⟩ = x.

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

(3) 1 · x = x and 0 · x = ⟨\underbrace{0, …, 0}_{n}⟩.

(4) (a · b) · x = a · (b · x).

(5) If a · x = ⟨\underbrace{0, …, 0}_{n}⟩, then a = 0 or x = ⟨\underbrace{0, …, 0}_{n}⟩.

(6) a · (x_{1} + x_{2}) = a · x_{1} + a · x_{2}.

(7) (a + b) · x = a · x + b · x.

(8) If a · x_{1} = a · x_{2}, then a = 0 or x_{1} = x_{2}.

Let us consider n and let x_{1}, x_{2} be elements of R^{n}. The functor Line(x_{1}, x_{2}) yields a subset of R^{n} and is defined by:

(Def. 1) Line(x_{1}, x_{2}) = {(1 − l_{1}) · x_{1} + l_{1} · x_{2}}.

Let us consider n and let x_{1}, x_{2} be elements of R^{n}. Observe that Line(x_{1}, x_{2}) is non empty.

The following proposition is true

(9) Line(x_{1}, x_{2}) = Line(x_{2}, x_{1}). Let us consider n and let x_{1}, x_{2} be elements of R^{n}. Let us observe that the

functor Line(x_{1}, x_{2}) is commutative.

One can prove the following propositions:

(10) x_{1} ∈ Line(x_{1}, x_{2}) and x_{2} ∈ Line(x_{1}, x_{2}).

(11) If y_{1} ∈ Line(x_{1}, x_{2}) and y_{2} ∈ Line(x_{1}, x_{2}), then Line(y_{1}, y_{2}) ⊆ Line(x_{1}, x_{2}).

(12) If y_{1} ∈ Line(x_{1}, x_{2}) and y_{2} ∈ Line(x_{1}, x_{2}) and y_{1} ≠ y_{2}, then

Line(x_{1}, x_{2}) ⊆ Line(y_{1}, y_{2}). Let us consider n and let A be a subset of R^{n}. We say that A is line if and

only if: (Def. 2) There exist x_{1}, x_{2} such that x_{1} ≠ x_{2} and A = Line(x_{1}, x_{2}).

We introduce A is a line as a synonym of A is line.

Next we state three propositions:

(13) Let A, C be subsets of R^{n} and given x_{1}, x_{2}. Suppose A is a line and C is a line and x_{1} ∈ A and x_{2} ∈ A and x_{1} ∈ C and x_{2} ∈ C. Then x_{1} = x_{2} or A = C.

(14) For every subset A of R^{n} such that A is a line there exist x_{1}, x_{2} such that x_{1} ∈ A and x_{2} ∈ A and x_{1} ≠ x_{2}.

(15) For every subset A of R^{n} such that A is a line there exists x_{2} such that

x_{1} ≠ x_{2} and x_{2} ∈ A. Let us consider n and let x be an element of R^{n}. The functor Rn2Fin(x)

yielding a finite sequence of elements of ℝ is defined by: (Def. 3) Rn2Fin(x) = x.

Let us consider n and let x be an element of R^{n}. The functor |x| yields a real number and is defined as follows:

(Def. 4) |x| = | Rn2Fin(x)|.

Let us consider n and let x_{1}, x_{2} be elements of R^{n}. The functor |(x_{1}, x_{2})| yielding a real number is defined by:

(Def. 5) |(x_{1}, x_{2})| = |(Rn2Fin(x_{1}), Rn2Fin(x_{2}))|.

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

We now state a number of propositions:

(16) For all elements x_{1}, x_{2} of R^{n} holds |(x_{1}, x_{2})| = \frac{1}{4} ·(|x_{1}+x_{2}|^{2} −|x_{1}−x_{2}|^{2}).

(17) For every element x of R^{n} holds |(x, x)| 0.

(18) For every element x of R^{n} holds |x|^{2} = |(x, x)|.

lines in n-dimensional euclidean spaces 373

(19) For every element x of R^{n} holds 0 |x|.

(20) For every element x of R^{n} holds |x| = \sqrt{|(x, x)|}.

(21) For every element x of R^{n} holds |(x, x)| = 0 iff |x| = 0.

(22) For every element x of R^{n} holds |(x, x)| = 0 iff x = ⟨\underbrace{0, …, 0}_{n}⟩.

(23) For every element x of R^{n} holds |(x, ⟨\underbrace{0, …, 0}_{n}⟩)| = 0.

(24) For every element x of R^{n} holds |(⟨\underbrace{0, …, 0}_{n}⟩, x)| = 0.

(25) For all elements x_{1}, x_{2}, x_{3} of R^{n} holds |(x_{1} + x_{2}, x_{3})| = |(x_{1}, x_{3})| + |(x_{2}, x_{3})|.

(26) For all elements x_{1}, x_{2} of R^{n} and for every real number a holds |(a · x_{1}, x_{2})| = a · |(x_{1}, x_{2})|.

(27) For all elements x_{1}, x_{2} of R^{n} and for every real number a holds |(x_{1}, a · x_{2})| = a · |(x_{1}, x_{2})|.

(28) For all elements x_{1}, x_{2} of R^{n} holds |(− x_{1}, x_{2})| = − |(x_{1}, x_{2})|.

(29) For all elements x_{1}, x_{2} of R^{n} holds |(x_{1}, − x_{2})| = − |(x_{1}, x_{2})|.

(30) For all elements x_{1}, x_{2} of R^{n} holds |(− x_{1}, − x_{2})| = |(x_{1}, x_{2})|.

(31) For all elements x_{1}, x_{2}, x_{3} of R^{n} holds |(x_{1} − x_{2}, x_{3})| = |(x_{1}, x_{3})| − |(x_{2}, x_{3})|.

(32) For all real numbers a, b and for all elements x_{1}, x_{2}, x_{3} of R^{n} holds |(a · x_{1} + b · x_{2}, x_{3})| = a · |(x_{1}, x_{3})| + b · |(x_{2}, x_{3})|.

(33) For all elements x_{1}, y_{1}, y_{2} of R^{n} holds |(x_{1}, y_{1} + y_{2})| = |(x_{1}, y_{1})| + |(x_{1}, y_{2})|.

(34) For all elements x_{1}, y_{1}, y_{2} of R^{n} holds |(x_{1}, y_{1} − y_{2})| = |(x_{1}, y_{1})| − |(x_{1}, y_{2})|.

(35) For all elements x_{1}, x_{2}, y_{1}, y_{2} of R^{n} holds |(x_{1}+x_{2}, y_{1}+y_{2})| = |(x_{1}, y_{1})|+ |(x_{1}, y_{2})| + |(x_{2}, y_{1})| + |(x_{2}, y_{2})|.

(36) For all elements x_{1}, x_{2}, y_{1}, y_{2} of R^{n} holds |(x_{1}−x_{2}, y_{1}−y_{2})| = (|(x_{1}, y_{1})|− |(x_{1}, y_{2})| − |(x_{2}, y_{1})|) + |(x_{2}, y_{2})|.

(37) For all elements x, y of R^{n} holds |(x + y, x + y)| = |(x, x)| + 2 · |(x, y)| + |(y, y)|.

(38) For all elements x, y of R^{n} holds |(x−y, x−y)| = (|(x, x)|−2·|(x, y)|)+ |(y, y)|.

(39) For all elements x, y of R^{n} holds |x + y|^{2} = |x|^{2} + 2 · |(x, y)| + |y|^{2}.

(40) For all elements x, y of R^{n} holds |x − y|^{2} = (|x|^{2} − 2 · |(x, y)|) + |y|^{2}.

(41) For all elements x, y of R^{n} holds |x + y|^{2} + |x − y|^{2} = 2 · (|x|^{2} + |y|^{2}).

(42) For all elements x, y of R^{n} holds |x + y|^{2} − |x − y|^{2} = 4 · |(x, y)|.

(43) For all elements x, y of R^{n} holds ||(x, y)|| |x| · |y|.

(44) For all elements x, y of R^{n} holds |x + y| |x| + |y|.

Let us consider n and let x_{1}, x_{2} be elements of R^{n}. We say that x_{1}, x_{2} are orthogonal if and only if:

(Def. 6) |(x_{1}, x_{2})| = 0.

Let us note that the predicate x_{1}, x_{2} are orthogonal is symmetric.

We now state the proposition

(45) Let R be a subset of ℝ and x_{1}, x_{2}, y_{1} be elements of R^{n}. Suppose R = {|y_{1} − x|; x ranges over elements of R^{n}: x ∈ Line(x_{1}, x_{2})}. Then there exists an element y_{2} of R^{n} such that y_{2} ∈ Line(x_{1}, x_{2}) and |y_{1}−y_{2}| = inf R and x_{1} − x_{2}, y_{1} − y_{2} are orthogonal.

Let us consider n and let p_{1}, p_{2} be points of E_{T}^{n}. The functor Line(p_{1}, p_{2}) yielding a subset of E_{T}^{n} is defined by:

(Def. 7) Line(p_{1}, p_{2}) = {(1 − l_{1}) · p_{1} + l_{1} · p_{2}}.

Let us consider n and let p_{1}, p_{2} be points of E_{T}^{n}. Observe that Line(p_{1}, p_{2}) is non empty.

In the sequel p_{1}, p_{2}, q_{1}, q_{2} are points of E_{T}^{n}. The following proposition is true

(46) Line(p_{1}, p_{2}) = Line(p_{2}, p_{1}).

Let us consider n and let p_{1}, p_{2} be points of E_{T}^{n}. Let us observe that the functor Line(p_{1}, p_{2}) is commutative.

One can prove the following three propositions:

(47) p_{1} ∈ Line(p_{1}, p_{2}) and p_{2} ∈ Line(p_{1}, p_{2}).

(48) If q_{1} ∈ Line(p_{1}, p_{2}) and q_{2} ∈ Line(p_{1}, p_{2}), then Line(q_{1}, q_{2}) ⊆ Line(p_{1}, p_{2}).

(49) If q_{1} ∈ Line(p_{1}, p_{2}) and q_{2} ∈ Line(p_{1}, p_{2}) and q_{1} ≠ q_{2}, then Line(p_{1}, p_{2}) ⊆

Line(q_{1}, q_{2}). Let us consider n and let A be a subset of E_{T}^{n}. We say that A is line if and

only if: (Def. 8) There exist p_{1}, p_{2} such that p_{1} ≠ p_{2} and A = Line(p_{1}, p_{2}).

We introduce A is a line as a synonym of A is line.

We now state three propositions:

(50) For all subsets A, C of E_{T}^{n} such that A is a line and C is a line and p_{1} ∈ A and p_{2} ∈ A and p_{1} ∈ C and p_{2} ∈ C holds p_{1} = p_{2} or A = C.

(51) For every subset A of E_{T}^{n} such that A is a line there exist p_{1}, p_{2} such that p_{1} ∈ A and p_{2} ∈ A and p_{1} ≠ p_{2}.

(52) For every subset A of E_{T}^{n} such that A is a line there exists p_{2} such that

p_{1} ≠ p_{2} and p_{2} ∈ A. Let us consider n and let p be a point of E_{T}^{n}. The functor TPn2Rn(p) yields

an element of R^{n} and is defined as follows:

lines in n-dimensional euclidean spaces 375

(Def. 9) TPn2Rn(p) = p. Let us consider n and let p be a point of E_{T}^{n}. The functor |p| yields a real

number and is defined as follows: (Def. 10) |p| = | TPn2Rn(p)|.

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

(Def. 11) |(p_{1}, p_{2})| = |(TPn2Rn(p_{1}), TPn2Rn(p_{2}))|. Let us observe that the functor |(p_{1}, p_{2})| is commutative.

Let us consider n and let p_{1}, p_{2} be points of E_{T}^{n}. We say that p_{1}, p_{2} are orthogonal if and only if:

(Def. 12) |(p_{1}, p_{2})| = 0.

Let us note that the predicate p_{1}, p_{2} are orthogonal is symmetric.

Next we state the proposition

(53) Let R be a subset of ℝ and p_{1}, p_{2}, q_{1} be points of E_{T}^{n}. Suppose R = {|q_{1} − p|; p ranges over points of E_{T}^{n}: p ∈ Line(p_{1}, p_{2})}. Then there exists a point q_{2} of E_{T}^{n} such that q_{2} ∈ Line(p_{1}, p_{2}) and |q_{1} −q_{2}| = inf R and p_{1} −p_{2}, q_{1} − q_{2} are orthogonal.

References

[1] Kanchun and Yatsuka Nakamura. The inner product of finite sequences and of points of n-dimensional topological space. Formalized Mathematics, 11(2):179–183, 2003.

[2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 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 from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

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

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

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

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

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

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

[12] Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics.

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

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

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

Banach Space of Absolute Summable Real Sequences

Yasumasa Suzuki Take, Yokosuka-shi Japan

Noboru Endou Gifu National College of Technology

Yasunari Shidama Shinshu University Nagano

Summary. A continuation of [5]. As the example of real norm spaces, we introduce the arithmetic addition and multiplication in the set of absolute summable real sequences and also introduce the norm. This set has the structure of the Banach space.

MML Identifier: RSSPACE3.

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

1. The Space of Absolute Summable Real Sequences

The subset the set of l1-real sequences of the linear space of real sequences is defined by the condition (Def. 1).

(Def. 1) Let x be a set. Then x ∈ the set of l1-real sequences if and only if x ∈ the

set of real sequences and id_{seq}(x) is absolutely summable. Let us observe that the set of l1-real sequences is non empty. One can prove the following two propositions:

(1) The set of l1-real sequences is linearly closed.

(2) ⟨the set of l1-real sequences, Zero (the set of l1-real sequences, the linear space of real sequences), Add (the set of l1-real sequences, the linear space of real sequences), Mult (the set of l1-real sequences, the linear space of real sequences)⟩ is a subspace of the linear space of real sequences.

One can check that ⟨the set of l1-real sequences, Zero (the set of l1-real sequences, the linear space of real sequences), Add (the set of l1real sequences, the linear space of real sequences), Mult (the set of l1-real sequences, the linear space of real sequences)⟩ is Abelian, add-associative, right zeroed, right complementable, and real linear space-like.

One can prove the following proposition

(3) ⟨the set of l1-real sequences, Zero (the set of l1-real sequences, the linear space of real sequences), Add (the set of l1-real sequences, the linear space of real sequences), Mult (the set of l1-real sequences, the linear space of real sequences)⟩ is a real linear space.

The function norm_{seq} from the set of l1-real sequences into ℝ is defined by: (Def. 2) For every set x such that x ∈ the set of l1-real sequences holds

norm_{seq}(x) = ∑|id_{seq}(x)|. Let X be a non empty set, let Z be an element of X, let A be a binary

operation on X, let M be a function from [: ℝ, X:] into X, and let N be a function from X into ℝ. One can check that ⟨X, Z, A, M, N⟩ is non empty.

Next we state four propositions:

(4) Let l be a normed structure. Suppose ⟨the carrier of l, the zero of l, the addition of l, the external multiplication of l⟩ is a real linear space. Then l is a real linear space.

(5) Let r_{1} be a sequence of real numbers. Suppose that for every natural number n holds r_{1}(n) = 0. Then r_{1} is absolutely summable and ∑|r_{1}| = 0.

(6) Let r_{1} be a sequence of real numbers. Suppose r_{1} is absolutely summable and ∑|r_{1}| = 0. Let n be a natural number. Then r_{1}(n) = 0.

(7) ⟨the set of l1-real sequences, Zero (the set of l1-real sequences, the linear space of real sequences), Add (the set of l1-real sequences, the linear space of real sequences), Mult (the set of l1-real sequences, the linear space of real sequences), norm_{seq}⟩ is a real linear space.

The non empty normed structure l1-Space is defined by the condition (Def. 3).

(Def. 3) l1-Space = ⟨the set of l1-real sequences, Zero (the set of l1-real sequences, the linear space of real sequences), Add (the set of l1-real sequences, the linear space of real sequences), Mult (the set of l1-real sequences, the linear space of real sequences), norm_{seq}⟩.

2. The Space is Banach Space

One can prove the following two propositions:

(8) The carrier of l1-Space = the set of l1-real sequences and for every set x holds x is an element of l1-Space iff x is a sequence of real numbers and id_{seq}(x) is absolutely summable and for every set x holds x is a vector of l1-Space iff x is a sequence of real numbers and id_{seq}(x) is absolutely summable and 0_{l1-Space} = Zeroseq and for every vector u of l1-Space holds u = id_{seq}(u) and for all vectors u, v of l1-Space holds u + v = id_{seq}(u) + id_{seq}(v) and for every real number r and for every vector u of l1-Space holds r · u = r id_{seq}(u) and for every vector u of l1-Space holds − u = − id_{seq}(u) and id_{seq}(− u) = − id_{seq}(u) and for all vectors u, v of l1-Space holds u − v = id_{seq}(u) − id_{seq}(v) and for every vector v of l1-Space holds id_{seq}(v) is absolutely summable and for every vector v of l1-Space holds ∥v∥ = ∑|id_{seq}(v)|.

(9) Let x, y be points of l1-Space and a be a real number. Then ∥x∥ = 0 iff x = 0_{l1-Space} and 0 ∥x∥ and ∥x + y∥ ∥x∥ + ∥y∥ and ∥a · x∥ = |a| · ∥x∥.

Let us observe that l1-Space is real normed space-like, real linear space-like, Abelian, add-associative, right zeroed, and right complementable.

Let X be a non empty normed structure and let x, y be points of X. The functor ρ(x, y) yields a real number and is defined by:

(Def. 4) ρ(x, y) = ∥x − y∥.

Let N_{1} be a non empty normed structure and let s_{1} be a sequence of N_{1}. We say that s_{1} is CCauchy if and only if the condition (Def. 5) is satisfied.

(Def. 5) Let r_{2} be a real number. Suppose r_{2} > 0. Then there exists a natural number k_{1} such that for all natural numbers n_{1}, m_{1} if n_{1} k_{1} and m_{1} k_{1}, then ρ(s_{1}(n_{1}), s_{1}(m_{1})) < r_{2}.

We introduce s_{1} is Cauchy sequence by norm as a synonym of s_{1} is CCauchy.

In the sequel N_{1} denotes a non empty real normed space and s_{2} denotes a sequence of N_{1}.

We now state two propositions:

(10) s_{2} is Cauchy sequence by norm if and only if for every real number r such that r > 0 there exists a natural number k such that for all natural numbers n, m such that n k and m k holds ∥s_{2}(n) − s_{2}(m)∥ < r.

(11) For every sequence v_{1} of l1-Space such that v_{1} is Cauchy sequence by norm holds v_{1} is convergent.

References

[1] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.

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

380 yasumasa suzuki et al.

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

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

[5] Noboru Endou, Yasumasa Suzuki, and Yasunari Shidama. Hilbert space of real sequences. Formalized Mathematics, 11(3):255–257, 2003.

[6] Noboru Endou, Yasumasa Suzuki, and Yasunari Shidama. Real linear space of real sequences. Formalized Mathematics, 11(3):249–253, 2003.

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

[8] Jarosław Kotowicz. Monotone real sequences. Subsequences. Formalized Mathematics, 1(3):471–475, 1990.

[9] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269–272, 1990.

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

[11] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111–115, 1991.

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

[13] Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics.

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

[15] Wojciech A. Trybulec. Subspaces and cosets of subspaces in real linear space. Formalized Mathematics, 1(2):297–301, 1990.

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

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

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

Cross Products and Tripple Vector Products in 3-dimensional Euclidean Space

Kanchun Shinshu University

Nagano Hiroshi Yamazaki Shinshu University Nagano Yatsuka Nakamura Shinshu University Nagano

Summary. First, we extend the basic theorems of 3-dimensional Euclidean space, and then define the cross product in the same space and relative vector relations using the above definition.

MML Identifier: EUCLID 5.

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

We adopt the following convention: x, y, z denote real numbers, x_{3}, y_{3} denote elements of ℝ, and p denotes a point of E_{T}^{3}.

We now state the proposition

(1) There exist x, y, z such that p = ⟨x, y, z⟩.

Let us consider p. The functor p_{1} yielding a real number is defined as follows: (Def. 1) For every finite sequence f such that p = f holds p_{1} = f(1).

The functor p_{2} yields a real number and is defined by: (Def. 2) For every finite sequence f such that p = f holds p_{2} = f(2).

The functor p_{3} yields a real number and is defined by: (Def. 3) For every finite sequence f such that p = f holds p_{3} = f(3).

Let us consider x, y, z. The functor [x, y, z] yields a point of E_{T}^{3} and is defined as follows:

(Def. 4) [x, y, z] = ⟨x, y, z⟩.

One can prove the following three propositions:

(2) [x, y, z]_{1} = x and [x, y, z]_{2} = y and [x, y, z]_{3} = z.

(3) p = [p_{1}, p_{2}, p_{3}].

(4) 0_{E_{T}^{3}} = [0, 0, 0].

We adopt the following rules: p_{1}, p_{2}, p_{3}, p_{4} are points of E_{T}^{3} and x_{1}, x_{2}, y_{1}, y_{2}, z_{1}, z_{2} are real numbers.

Next we state several propositions:

(5) p_{1} + p_{2} = [(p_{1})_{1} + (p_{2})_{1}, (p_{1})_{2} + (p_{2})_{2}, (p_{1})_{3} + (p_{2})_{3}].

(6) [x_{1}, y_{1}, z_{1}] + [x_{2}, y_{2}, z_{2}] = [x_{1} + x_{2}, y_{1} + y_{2}, z_{1} + z_{2}].

(7) x · p = [x · p_{1}, x · p_{2}, x · p_{3}].

(8) x · [x_{1}, y_{1}, z_{1}] = [x · x_{1}, x · y_{1}, x · z_{1}].

(9) (x · p)_{1}= x · p_{1} and (x · p)_{2}= x · p_{2} and (x · p)_{3}= x · p_{3}.

(10) − p = [− p_{1}, − p_{2}, − p_{3}].

(11) − [x_{1}, y_{1}, z_{1}] = [− x_{1}, − y_{1}, − z_{1}].

(12) p_{1} − p_{2} = [(p_{1})_{1} − (p_{2})_{1}, (p_{1})_{2} − (p_{2})_{2}, (p_{1})_{3} − (p_{2})_{3}].

(13) [x_{1}, y_{1}, z_{1}] − [x_{2}, y_{2}, z_{2}] = [x_{1} − x_{2}, y_{1} − y_{2}, z_{1} − z_{2}].

Let us consider p_{1}, p_{2}. The functor p_{1} × p_{2} yielding a point of E_{T}^{3} is defined by:

(Def. 5) p_{1} × p_{2} = [(p_{1})_{2} · (p_{2})_{3} − (p_{1})_{3} · (p_{2})_{2}, (p_{1})_{3} · (p_{2})_{1} − (p_{1})_{1} · (p_{2})_{3}, (p_{1})_{1} ·

(p_{2})_{2} − (p_{1})_{2} · (p_{2})_{1}]. The following propositions are true:

(14) If p = [x, y, z], then p_{1} = x and p_{2} = y and p_{3} = z.

(15) [x_{1}, y_{1}, z_{1}] × [x_{2}, y_{2}, z_{2}] = [y_{1} · z_{2} − z_{1} · y_{2}, z_{1} · x_{2} − x_{1} · z_{2}, x_{1} · y_{2} − y_{1} · x_{2}].

(16) (x · p_{1}) × p_{2} = x · (p_{1} × p_{2}) and (x · p_{1}) × p_{2} = p_{1} × (x · p_{2}).

(17) p_{1} × p_{2} = − p_{2} × p_{1} .

(18) (− p_{1}) × p_{2} = p_{1} × − p_{2}.

(19) [0, 0, 0] × [x, y, z] = 0_{E_{T}^{3}}.

(20) [x_{1}, 0, 0] × [x_{2}, 0, 0] = 0_{E_{T}^{3}}.

(21) [0, y_{1}, 0] × [0, y_{2}, 0] = 0_{E_{T}^{3}}.

(22) [0, 0, z_{1}] × [0, 0, z_{2}] = 0_{E_{T}^{3}}.

(23) p_{1} × (p_{2} + p_{3}) = p_{1} × p_{2} + p_{1} × p_{3}.

(24) (p_{1} + p_{2}) × p_{3} = p_{1} × p_{3} + p_{2} × p_{3}.

(25) p_{1} × p_{1} = 0_{E_{T}^{3}}.

(26) (p_{1} + p_{2}) × (p_{3} + p_{4}) = p_{1} × p_{3} + p_{1} × p_{4} + p_{2} × p_{3} + p_{2} × p_{4}.

(27) p = ⟨p_{1}, p_{2}, p_{3}⟩.

(28) For all finite sequences f_{1}, f_{2} of elements of ℝ such that lenf_{1} = 3 and lenf_{2} = 3 holds f_{1} • f_{2} = ⟨f_{1}(1) · f_{2}(1), f_{1}(2) · f_{2}(2), f_{1}(3) · f_{2}(3)⟩.

(29) |(p_{1}, p_{2})| = (p_{1})_{1} · (p_{2})_{1} + (p_{1})_{2} · (p_{2})_{2} + (p_{1})_{3} · (p_{2})_{3}.

(30) |([x_{1}, x_{2}, x_{3}], [y_{1}, y_{2}, y_{3}])| = x_{1} · y_{1} + x_{2} · y_{2} + x_{3} · y_{3}.

cross products and tripple vector products … 383

Let us consider p_{1}, p_{2}, p_{3}. The functor ⟨|p_{1}, p_{2}, p_{3}|⟩ yielding a real number is defined as follows:

(Def. 6) ⟨|p_{1}, p_{2}, p_{3}|⟩ = |(p_{1}, p_{2} × p_{3})|. The following propositions are true:

(31) ⟨|p_{1}, p_{1}, p_{2}|⟩ = 0 and ⟨|p_{2}, p_{1}, p_{2}|⟩ = 0.

(32) p_{1} × (p_{2} × p_{3}) = |(p_{1}, p_{3})| · p_{2} − |(p_{1}, p_{2})| · p_{3}.

(33) ⟨|p_{1}, p_{2}, p_{3}|⟩ = ⟨|p_{2}, p_{3}, p_{1}|⟩.

(34) ⟨|p_{1}, p_{2}, p_{3}|⟩ = ⟨|p_{3}, p_{1}, p_{2}|⟩.

(35) ⟨|p_{1}, p_{2}, p_{3}|⟩ = |(p_{1} × p_{2}, p_{3})|.

References

[1] Kanchun and Yatsuka Nakamura. The inner product of finite sequences and of points of n-dimensional topological space. Formalized Mathematics, 11(2):179–183, 2003.

[2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 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. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

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

[6] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 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ł. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

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

[10] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269–272, 1990.

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

[12] Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics.

[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.

Calculation of Matrices of Field Elements. Part I

Yatsuka Nakamura Shinshu University Nagano Hiroshi Yamazaki Shinshu University Nagano

Summary. This article gives property of calculation of matrices.

MML Identifier: MATRIX 4.

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

In this paper i denotes a natural number. Let K be a field and let M_{1}, M_{2} be matrices over K. The functor M_{1} − M_{2}

yielding a matrix over K is defined by: (Def. 1) M_{1} − M_{2} = M_{1} + − M_{2}.

One can prove the following propositions:

(1) For every field K and for every matrix M over K such that lenM > 0 holds − − M = M.

(2) For every field K and for every matrix M over K such that lenM > 0

holds M + − M = ( \begin{matrix}0 & … & 0 \\ ⋮ & ... & ⋮ \\ 0 & … & 0 \end{matrix} )_{K}^{(len M)×(width M)} .

(3) For every field K and for every matrix M over K such that lenM > 0

holds M − M = ( \begin{matrix}0 & … & 0 \\ ⋮ & ... & ⋮ \\ 0 & … & 0 \end{matrix} )_{K}^{(len M)×(width M)} .

(4) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. Suppose lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0 and M_{1} + M_{3} = M_{2} + M_{3}. Then M_{1} = M_{2}.

(5) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{2} > 0 holds M_{1} − − M_{2} = M_{1} + M_{2}.

(6) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 and M_{1} = M_{1} + M_{2}

holds M_{2} = ( \begin{matrix}0 & … & 0 \\ ⋮ & ... & ⋮ \\ 0 & … & 0 \end{matrix} )_{K}^{(len M_{1})×(width M_{1})} .

(7) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 and M_{1}−M_{2} =

( \begin{matrix}0 & … & 0 \\ ⋮ & ... & ⋮ \\ 0 & … & 0 \end{matrix} )_{K}^{(len M_{1})×(width M_{1})} holds M_{1} = M_{2}.

(8) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 and M_{1}+M_{2} =

( \begin{matrix}0 & … & 0 \\ ⋮ & ... & ⋮ \\ 0 & … & 0 \end{matrix} )_{K}^{(len M_{1})×(width M_{1})} holds M_{2} = − M_{1}.

(9) For all natural numbers n, m and for every field K such that n > 0 holds

− ( \begin{matrix}0 & … & 0 \\ ⋮ & ... & ⋮ \\ 0 & … & 0 \end{matrix} )_{K}^{n×m} = ( \begin{matrix}0 & … & 0 \\ ⋮ & ... & ⋮ \\ 0 & … & 0 \end{matrix} )_{K}^{n×m} .

(10) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 and M_{2} − M_{1} = M_{2}

holds M_{1} = ( \begin{matrix}0 & … & 0 \\ ⋮ & ... & ⋮ \\ 0 & … & 0 \end{matrix} )_{K}^{(len M_{1})×(width M_{1})} .

(11) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds M_{1} = M_{1} −(M_{2} − M_{2}).

(12) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds − (M_{1} + M_{2}) = − M_{1} + − M_{2}.

(13) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds M_{1}−(M_{1}−M_{2}) = M_{2}.

(14) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. Suppose lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0 and M_{1} − M_{3} = M_{2} − M_{3}. Then M_{1} = M_{2}.

calculation of matrices of field elements. … 387

(15) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. Suppose lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0 and M_{3} − M_{1} = M_{3} − M_{2}. Then M_{1} = M_{2}.

(16) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then M_{1} − M_{2} − M_{3} = M_{1} − M_{3} − M_{2}.

(17) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then M_{1} − M_{3} = M_{1} − M_{2} − (M_{3} − M_{2}).

(18) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then M_{3} − M_{1} − (M_{3} − M_{2}) = M_{2} − M_{1}.

(19) Let K be a field and M_{1}, M_{2}, M_{3}, M_{4} be matrices over K. Suppose lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and lenM_{3} = lenM_{4} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and widthM_{3} = widthM_{4} and lenM_{1} > 0 and M_{1} − M_{2} = M_{3} − M_{4}. Then M_{1} − M_{3} = M_{2} − M_{4}.

(20) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds M_{1} = M_{1} +(M_{2} − M_{2}).

(21) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds M_{1} = (M_{1}+M_{2})− M_{2}.

(22) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds M_{1} = (M_{1}−M_{2})+ M_{2}.

(23) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then M_{1} + M_{3} = M_{1} + M_{2} + (M_{3} − M_{2}).

(24) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then (M_{1} + M_{2}) − M_{3} = (M_{1} − M_{3}) + M_{2}.

(25) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then (M_{1} − M_{2}) + M_{3} = (M_{3} − M_{2}) + M_{1}.

(26) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then M_{1} + M_{3} = (M_{1} + M_{2}) − (M_{2} − M_{3}).

(27) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3}

and lenM_{1} > 0, then M_{1} − M_{3} = (M_{1} + M_{2}) − (M_{3} + M_{2}).

(28) Let K be a field and M_{1}, M_{2}, M_{3}, M_{4} be matrices over K. Suppose lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and lenM_{3} = lenM_{4} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and widthM_{3} = widthM_{4} and lenM_{1} > 0 and M_{1} + M_{2} = M_{3} + M_{4}. Then M_{1} − M_{3} = M_{4} − M_{2}.

(29) Let K be a field and M_{1}, M_{2}, M_{3}, M_{4} be matrices over K. Suppose lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and lenM_{3} = lenM_{4} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and widthM_{3} = widthM_{4} and lenM_{1} > 0 and M_{1} − M_{3} = M_{4} − M_{2}. Then M_{1} + M_{2} = M_{3} + M_{4}.

(30) Let K be a field and M_{1}, M_{2}, M_{3}, M_{4} be matrices over K. Suppose lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and lenM_{3} = lenM_{4} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and widthM_{3} = widthM_{4} and lenM_{1} > 0 and M_{1} + M_{2} = M_{3} − M_{4}. Then M_{1} + M_{4} = M_{3} − M_{2}.

(31) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then M_{1} − (M_{2} + M_{3}) = M_{1} − M_{2} − M_{3}.

(32) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then M_{1} − (M_{2} − M_{3}) = (M_{1} − M_{2}) + M_{3}.

(33) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then M_{1} − (M_{2} − M_{3}) = M_{1} + (M_{3} − M_{2}).

(34) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then M_{1} − M_{3} = (M_{1} − M_{2}) + (M_{2} − M_{3}).

(35) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0 and − M_{1} = − M_{2}, then M_{1} = M_{2}.

(36) For every field K and for every matrix M over K such that lenM > 0

and − M = ( \begin{matrix}0 & … & 0 \\ ⋮ & ... & ⋮ \\ 0 & … & 0 \end{matrix} )_{K}^{(len M)×(width M)}

holds M = ( \begin{matrix}0 & … & 0 \\ ⋮ & ... & ⋮ \\ 0 & … & 0 \end{matrix} )_{K}^{(len M)×(width M)} .

(37) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 and M_{1} + − M_{2} =

( \begin{matrix}0 & … & 0 \\ ⋮ & ... & ⋮ \\ 0 & … & 0 \end{matrix} )_{K}^{(len M_{1})×(width M_{1})} holds M_{1} = M_{2}.

(38) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds M_{1} = M_{1} + M_{2} + − M_{2}.

(39) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds M_{1} = M_{1} +(M_{2} + − M_{2}).

(40) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds M_{1} = − M_{2}+M_{1}+ M_{2}.

(41) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds − (− M_{1} + M_{2}) = M_{1} + − M_{2}.

(42) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds M_{1} + M_{2} = − (− M_{1} + − M_{2}).

(43) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds − (M_{1} − M_{2}) = M_{2} − M_{1}.

(44) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds − M_{1} − M_{2} = − M_{2} − M_{1}.

(45) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds M_{1} = − M_{2} − (− M_{1} − M_{2}).

(46) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then − M_{1} − M_{2} − M_{3} = − M_{1} − M_{3} − M_{2}.

(47) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then − M_{1} − M_{2} − M_{3} = − M_{2} − M_{3} − M_{1}.

(48) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then − M_{1} − M_{2} − M_{3} = − M_{3} − M_{2} − M_{1}.

(49) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. If lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0, then M_{3} − M_{1} − (M_{3} − M_{2}) = − (M_{1} − M_{2}) .

(50) For every field K and for every matrix M over K such that lenM > 0

holds ( \begin{matrix}0 & … & 0 \\ ⋮ & ... & ⋮ \\ 0 & … & 0 \end{matrix} )_{K}^{(len M)×(width M)} − M = − M.

(51) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds M_{1} + M_{2} = M_{1} − − M_{2}.

(52) For every field K and for all matrices M_{1}, M_{2} over K such that lenM_{1} = lenM_{2} and widthM_{1} = widthM_{2} and lenM_{1} > 0 holds M_{1} = M_{1} −(M_{2} + − M_{2}).

(53) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. Suppose lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0 and M_{1} − M_{3} = M_{2} + − M_{3}. Then M_{1} = M_{2}.

(54) Let K be a field and M_{1}, M_{2}, M_{3} be matrices over K. Suppose lenM_{1} = lenM_{2} and lenM_{2} = lenM_{3} and widthM_{1} = widthM_{2} and widthM_{2} = widthM_{3} and lenM_{1} > 0 and M_{3} − M_{1} = M_{3} + − M_{2}. Then M_{1} = M_{2}.

(55) Let K be a field and A, B be matrices over K. If lenA = lenB and widthA = widthB, then the indices of A = the indices of B.

(56) Let K be a field and x, y, z be finite sequences of elements of the carrier of K. If lenx = leny and leny = lenz, then (x + y) • z = x • z + y • z.

(57) Let K be a field and x, y, z be finite sequences of elements of the carrier of K. If lenx = leny and leny = lenz, then z • (x + y) = z • x + z • y.

(58) Let D be a non empty set and M be a matrix over D. Suppose lenM > 0. Let n be a natural number. Then M is a matrix over D of dimension n × widthM if and only if n = lenM.

(59) Let K be a field, j be a natural number, and A, B be matrices over K. Suppose lenA = lenB and widthA = widthB and there exists a natural number j such that ⟨⟨i, j⟩⟩ ∈ the indices of A. Then Line(A + B, i) = Line(A, i) + Line(B, i).

(60) Let K be a field, j be a natural number, and A, B be matrices over K. Suppose lenA = lenB and widthA = widthB and there exists a natural number i such that ⟨⟨i, j⟩⟩∈ the indices of A. Then (A + B)_{□,j} = A_{□,j} + B_{□,j}.

(61) Let V_{1} be a field and P_{1}, P_{2} be finite sequences of elements of the carrier of V_{1}. If lenP_{1} = lenP_{2}, then ∑(P_{1} + P_{2}) = ∑ P_{1} + ∑ P_{2}.

(62) Let K be a field and A, B, C be matrices over K. If lenB = lenC and widthB = widthC and widthA = lenB and lenA > 0 and lenB > 0, then A · (B + C) = A · B + A · C.

(63) Let K be a field and A, B, C be matrices over K. If lenB = lenC and

calculation of matrices of field elements. … 391

widthB = widthC and lenA = widthB and lenB > 0 and lenA > 0, then (B + C) · A = B · A + C · A.

(64) Let K be a field, n, m, k be natural numbers, M_{1} be a matrix over K of dimension n × m, and M_{2} be a matrix over K of dimension m × k. Suppose widthM_{1} = lenM_{2} and 0 < lenM_{1} and 0 < lenM_{2}. Then M_{1}·M_{2} is a matrix over K of dimension n × k.

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. Binary operations applied to finite sequences. Formalized Mathematics, 1(4):643–649, 1990.

[3] Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 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] Katarzyna Jankowska. Matrices. Abelian group of matrices. Formalized Mathematics, 2(4):475–480, 1991.

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

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

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

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

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

[12] Katarzyna Zawadzka. The sum and product of finite sequences of elements of a field. Formalized Mathematics, 3(2):205–211, 1992.

[13] Katarzyna Zawadzka. The product and the determinant of matrices with entries in a field. Formalized Mathematics, 4(1):1–8, 1993.

Lattice of Fuzzy Sets^{1}

Takashi Mitsuishi Miyagi University

Grzegorz Bancerek Białystok Technical University

Summary. This article concerns a connection of fuzzy logic and lattice theory. Namely, the fuzzy sets form a Heyting lattice with union and intersection of fuzzy sets as meet and join operations. The lattice of fuzzy sets is defined as the product of interval posets. As the final result, we have characterized the composition of fuzzy relations in terms of lattice theory and proved its associativity.

MML Identifier: LFUZZY 0.

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

1. Posets of Real Numbers

Let R be a relational structure. We say that R is real if and only if the conditions (Def. 1) are satisfied.

(Def. 1)(i) The carrier of R ⊆ ℝ, and

(ii) for all real numbers x, y such that x ∈ the carrier of R and y ∈ the

carrier of R holds ⟨⟨x, y⟩⟩∈ the internal relation of R iff x y. Let R be a relational structure. We say that R is interval if and only if:

(Def. 2) R is real and there exist real numbers a, b such that a b and the carrier

of R = [a, b]. Let us mention that every relational structure which is interval is also real

and non empty.

1This work has been partially supported by the Polish Academy of Sciences and the Japan Society for the Promotion of Science (JSPS Grant 0324101 and JSPS Grant-in-aid 15700195)

when the first author was visiting Białystok Technical University as postdoctoral fellow.

Let us observe that every relational structure which is empty is also real. One can prove the following proposition

(1) For every subset X of ℝ there exists a strict relational structure R such that the carrier of R = X and R is real.

Let us note that there exists a relational structure which is interval and strict.

The following proposition is true

(2) Let R_{1}, R_{2} be real relational structures. Suppose the carrier of R_{1} = the carrier of R_{2}. Then the relational structure of R_{1} = the relational structure of R_{2}.

Let R be a non empty real relational structure. Observe that every element of R is real.

Let X be a subset of ℝ. The functor RealPosetX yields a real strict relational structure and is defined as follows:

(Def. 3) The carrier of RealPosetX = X. Let X be a non empty subset of ℝ. Note that RealPosetX is non empty. Let R be a relational structure and let x, y be elements of R. We introduce

x ⪯ y and y ⪰ x as synonyms of x y.

Let x, y be real numbers. We introduce x _{ℝ} y and y _{ℝ} x as synonyms of x y. We introduce y <_{ℝ} x and x >_{ℝ} y as antonyms of x y.

We now state the proposition

(3) For every non empty real relational structure R and for all elements x, y of R holds x _{ℝ} y iff x ⪯ y.

Let us observe that every relational structure which is real is also reflexive, antisymmetric, and transitive.

Let us observe that every real non empty relational structure is connected. Let R be a non empty real relational structure and let x, y be elements of

R. Then max(x, y) is an element of R.

Let R be a non empty real relational structure and let x, y be elements of R. Then min(x, y) is an element of R.

Let us note that every real non empty relational structure has l.u.b.’s and g.l.b.’s.

We follow the rules: x, y denote real numbers, R denotes a real non empty relational structure, and a, b denote elements of R.

One can prove the following four propositions:

(4) a ⊔ b = max(a, b).

(5) a ⊓ b = min(a, b).

(6) There exists x such that x ∈ the carrier of R and for every y such that y ∈ the carrier of R holds x y if and only if R is lower-bounded.

(7) There exists x such that x ∈ the carrier of R and for every y such that y ∈ the carrier of R holds x y if and only if R is upper-bounded.

Let us observe that every non empty relational structure which is interval is also bounded.

The following proposition is true

(8) For every interval non empty relational structure R and for every set X holds sup X exists in R.

Let us observe that every interval non empty relational structure is complete. Let us note that every chain is distributive. One can check that every interval non empty relational structure is Heyting. One can verify that [0, 1] is non empty. Let us observe that RealPoset[0, 1] is interval.

2. Product of Heyting Lattices

We now state several propositions:

(9) Let I be a non empty set and J be a relational structure yielding nonempty reflexive-yielding many sorted set indexed by I. Suppose that for every element i of I holds J(i) is a sup-semilattice. Then ∏ J has l.u.b.’s.

(10) Let I be a non empty set and J be a relational structure yielding nonempty reflexive-yielding many sorted set indexed by I. Suppose that for every element i of I holds J(i) is a semilattice. Then ∏ J has g.l.b.’s.

(11) Let I be a non empty set and J be a relational structure yielding nonempty reflexive-yielding many sorted set indexed by I. Suppose that for every element i of I holds J(i) is a semilattice. Let f, g be elements of ∏ J and i be an element of I. Then (f ⊓ g)(i) = f(i) ⊓ g(i).

(12) Let I be a non empty set and J be a relational structure yielding nonempty reflexive-yielding many sorted set indexed by I. Suppose that for every element i of I holds J(i) is a sup-semilattice. Let f, g be elements of ∏ J and i be an element of I. Then (f ⊔ g)(i) = f(i) ⊔ g(i).

(13) Let I be a non empty set and J be a relational structure yielding nonempty reflexive-yielding many sorted set indexed by I. Suppose that for every element i of I holds J(i) is a Heyting complete lattice. Then ∏ J is complete and Heyting.

Let A be a non empty set and let R be a complete Heyting lattice. Observe that R^{A} is Heyting.

3. Lattice of Fuzzy Sets

Let A be a non empty set. The functor FuzzyLatticeA yielding a Heyting complete lattice is defined by:

(Def. 4) FuzzyLatticeA = (RealPoset[0, 1])^{A}.

We now state the proposition

(14) For every non empty set A holds the carrier of FuzzyLatticeA = [0, 1]^{A}. Let A be a non empty set. Note that FuzzyLatticeA is constituted functions. Next we state the proposition

(15) Let R be a complete Heyting lattice, X be a subset of R, and y be an element of R. Then ⨆_{R} X ⊓ y = ⨆_{R}{x ⊓ y; x ranges over elements of R: x ∈ X}.

Let X be a non empty set and let a be an element of FuzzyLatticeX. The functor ^{@}a yields a membership function of X and is defined by:

(Def. 5) ^{@}a = a.

Let X be a non empty set and let f be a membership function of X. The functor f^{@} yielding an element of FuzzyLatticeX is defined by:

(Def. 6) f^{@} = f.

Let X be a non empty set, let f be a membership function of X, and let x be an element of X. Then f(x) is an element of RealPoset[0, 1].

Let X be a non empty set, let f be an element of FuzzyLatticeX, and let x be an element of X. Then f(x) is an element of RealPoset[0, 1].

For simplicity, we follow the rules: C is a non empty set, c is an element of C, f, g are membership functions of C, and s, t are elements of FuzzyLatticeC.

Next we state several propositions:

(16) For every c holds f(c) _{ℝ} g(c) iff f^{@} ⪯ g^{@}.

(17) s ⪯ t iff for every c holds (^{@}s)(c) _{ℝ} (^{@}t)(c).

(18) max(f, g) = f^{@} ⊔ g^{@}.

(19) s ⊔ t = max(^{@}s,^{@}t).

(20) min(f, g) = f^{@} ⊓ g^{@}.

(21) s ⊓ t = min(^{@}s,^{@}t).

4. Associativity of Composition of Fuzzy Relations

In this article we present several logical schemes. The scheme SupDistributivity deals with a complete lattice A, non empty sets B, C, a binary functor F yielding an element of A, and two unary predicates P, Q, and states that:

⨆_{A}{⨆_{A}{F(x, y); y ranges over elements of C : Q[y]}; x ranges over elements of B : P[x]} = ⨆_{A}{F(x, y); x ranges over elements of B, y ranges over elements of C : P[x] ∧ Q[y]}

for all values of the parameters.

The scheme SupDistributivity’ deals with a complete lattice A, non empty sets B, C, a binary functor F yielding an element of A, and two unary predicates P, Q, and states that:

⨆_{A}{⨆_{A}{F(x, y); x ranges over elements of B : P[x]}; y ranges over elements of C : Q[y]} = ⨆_{A}{F(x, y); x ranges over elements of B, y ranges over elements of C : P[x] ∧ Q[y]}

for all values of the parameters.

The scheme FraenkelF’R’ deals with a non empty set A, a non empty set B, two binary functors F and G yielding sets, and a binary predicate P, and states that:

{F(u_{1}, v_{1}); u_{1} ranges over elements of A, v_{1} ranges over elements of B : P[u_{1}, v_{1}]} = {G(u_{2}, v_{2}); u_{2} ranges over elements of A, v_{2} ranges over elements of B : P[u_{2}, v_{2}]}

provided the parameters meet the following condition:

• For every element u of A and for every element v of B such that P[u, v] holds F(u, v) = G(u, v).

The scheme FraenkelF6”R deals with a non empty set A, a non empty set B, two binary functors F and G yielding sets, and two binary predicates P, Q, and states that:

{F(u_{1}, v_{1}); u_{1} ranges over elements of A, v_{1} ranges over elements of B : P[u_{1}, v_{1}]} = {G(u_{2}, v_{2}); u_{2} ranges over elements of A, v_{2} ranges over elements of B : Q[u_{2}, v_{2}]}

provided the following requirements are met:

• For every element u of A and for every element v of B holds P[u, v] iff Q[u, v], and

• For every element u of A and for every element v of B such that P[u, v] holds F(u, v) = G(u, v).

The scheme SupCommutativity deals with a complete lattice A, non empty sets B, C, two binary functors F and G yielding elements of A, and two unary predicates P, Q, and states that:

⨆_{A}{⨆_{A}{F(x, y); y ranges over elements of C : Q[y]}; x ranges over elements of B : P[x]} = ⨆_{A}{⨆_{A}{G(x′, y′); x′ranges over elements of B : P[x′]}; y′ ranges over elements of C : Q[y′]}

provided the parameters meet the following condition:

• For every element x of B and for every element y of C such that P[x] and Q[y] holds F(x, y) = G(x, y).

One can prove the following propositions:

398 takashi mitsuishi and grzegorz bancerek

(22) Let X, Y, Z be non empty sets, R be a membership function of X, Y, S be a membership function of Y, Z, x be an element of X, and z be an element of Z. Then (R S)(⟨⟨x, z⟩⟩) = ⨆_{RealPoset [0,1]}{R(⟨⟨x, y⟩⟩) ⊓ S(⟨⟨y, z⟩⟩) : y ranges over elements of Y }.

(23) Let X, Y, Z, W be non empty sets, R be a membership function of X, Y, S be a membership function of Y, Z, and T be a membership function of Z, W. Then (R S) T = R (S T).

References

[1] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.

[2] Grzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719–725, 1991.

[3] Grzegorz Bancerek. Bounds in posets and relational substructures. Formalized Mathematics, 6(1):81–91, 1997.

[4] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93–107, 1997.

[5] Grzegorz Bancerek. The “way-below” relation. Formalized Mathematics, 6(1):169–176, 1997.

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

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

[8] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990.

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

[10] Czesław Byliński. Galois connections. Formalized Mathematics, 6(1):131–143, 1997.

[11] Noboru Endou, Takashi Mitsuishi, and Keiji Ohkubo. Properties of fuzzy relation. Formalized Mathematics, 9(4):691–695, 2001.

[12] Adam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Formalized Mathematics, 6(1):117–121, 1997.

[13] Takashi Mitsuishi, Noboru Endou, and Yasunari Shidama. The concept of fuzzy set and membership function and basic properties of fuzzy set operation. Formalized Mathematics, 9(2):351–356, 2001.

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

[15] Konrad Raczkowski and Paweł Sadowski. Topological properties of subsets in real numbers. Formalized Mathematics, 1(4):777–780, 1990.

[16] Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics.

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

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

[19] Andrzej Trybulec. Many-sorted sets. Formalized Mathematics, 4(1):15–22, 1993.

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

[21] Wojciech A. Trybulec. Partially ordered sets. Formalized Mathematics, 1(2):313–319, 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.

[24] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.

On the Kuratowski Limit Operators^{1}

Adam Grabowski University of Białystok

Summary. In the paper we give formal descriptions of the two Kuratowski limit oprators: Li S and Ls S, where S is an arbitrary sequence of subsets of a fixed topological space. In the two last sections we prove basic properties of these lower and upper topological limits, which may be found e.g. in [19]. In the sections 2–4, we present three operators which are associated in some sense with the above mentioned, that is lim inf F, lim sup F, and limes F, where F is a sequence of subsets of a fixed 1-sorted structure.

MML Identifier: KURATO 2.

The articles [30], [33], [2], [29], [9], [1], [22], [24], [35], [12], [34], [6], [4], [18], [8], [7], [16], [5], [13], [25], [31], [21], [10], [23], [14], [15], [20], [17], [27], [28], [26], [11], [3], and [32] provide the notation and terminology for this paper.

1. Preliminaries

One can prove the following four propositions:

(1) For all sets X, x and for every subset A of X such that x ∉ A and x ∈ X holds x ∈ A^{c}.

(2) For every function F and for every set i such that i ∈ domF holds ⋂ F ⊆ F (i).

(3) Let T be a non empty 1-sorted structure and S_{1}, S_{2} be sequences of subsets of the carrier of T. Then S_{1} = S_{2} if and only if for every natural number n holds S_{1}(n) = S_{2}(n).

(4) For all sets A, B, C, D such that A meets B and C meets D holds [: A, C:] meets [: B, D:].

1This work has been partially supported by the CALCULEMUS grant HPRN-CT-2000-00102.

Let X be a 1-sorted structure. Note that every sequence of subsets of the carrier of X is non empty.

Let T be a non empty 1-sorted structure. One can check that there exists a sequence of subsets of the carrier of T which is non-empty.

Let T be a non empty 1-sorted structure. (Def. 1) A sequence of subsets of the carrier of T is said to be a sequence of

subsets of T. In this article we present several logical schemes. The scheme LambdaSSeq

deals with a non empty 1-sorted structure A and a unary functor F yielding a subset of A, and states that:

There exists a sequence f of subsets of A such that for every natural number n holds f(n) = F(n)

for all values of the parameters.

The scheme ExTopStrSeq deals with a non empty topological space A and a unary functor F yielding a subset of A, and states that:

There exists a sequence S of subsets of the carrier of A such that for every natural number n holds S(n) = F(n)

for all values of the parameters.

We now state the proposition

(5) Let X be a non empty 1-sorted structure and F be a sequence of subsets of the carrier of X. Then rngF is a family of subsets of X.

Let X be a non empty 1-sorted structure and let F be a sequence of subsets of the carrier of X. Then ⋃ F is a subset of X. Then ⋂ F is a subset of X.

2. Lower and Upper Limit of Sequences of Subsets

Let X be a non empty set, let S be a function from ℕ into X, and let k be a natural number. The functor S ↑ k yields a function from ℕ into X and is defined as follows:

(Def. 2) For every natural number n holds (S ↑ k)(n) = S(n + k).

Let X be a non empty 1-sorted structure and let F be a sequence of subsets of the carrier of X. The functor lim inf F yields a subset of X and is defined as follows:

(Def. 3) There exists a sequence f of subsets of X such that lim inf F = ⋃ f and

for every natural number n holds f(n) = ⋂(F ↑ n). The functor lim supF yields a subset of X and is defined by:

(Def. 4) There exists a sequence f of subsets of X such that lim supF = ⋂ f and

for every natural number n holds f(n) = ⋃(F ↑ n). Next we state a number of propositions:

(6) Let X be a non empty 1-sorted structure, F be a sequence of subsets of the carrier of X, and x be a set. Then x ∈ ⋂ F if and only if for every natural number z holds x ∈ F (z).

(7) Let X be a non empty 1-sorted structure, F be a sequence of subsets of the carrier of X, and x be a set. Then x ∈ lim inf F if and only if there exists a natural number n such that for every natural number k holds x ∈ F (n + k).

(8) Let X be a non empty 1-sorted structure, F be a sequence of subsets of the carrier of X, and x be a set. Then x ∈ lim supF if and only if for every natural number n there exists a natural number k such that x ∈ F (n + k).

(9) For every non empty 1-sorted structure X and for every sequence F of subsets of the carrier of X holds lim inf F ⊆ lim supF.

(10) For every non empty 1-sorted structure X and for every sequence F of subsets of the carrier of X holds ⋂ F ⊆ lim inf F.

(11) For every non empty 1-sorted structure X and for every sequence F of subsets of the carrier of X holds lim supF ⊆ ⋃ F.

(12) For every non empty 1-sorted structure X and for every sequence F of subsets of the carrier of X holds lim inf F = (lim supComplementF)^{c}.

(13) Let X be a non empty 1-sorted structure and A, B, C be sequences of subsets of the carrier of X. If for every natural number n holds C(n) = A(n) ∩ B(n), then lim inf C = lim inf A ∩ lim inf B.

(14) Let X be a non empty 1-sorted structure and A, B, C be sequences of subsets of the carrier of X. If for every natural number n holds C(n) = A(n) ∪ B(n), then lim supC = lim supA ∪ lim supB.

(15) Let X be a non empty 1-sorted structure and A, B, C be sequences of subsets of the carrier of X. If for every natural number n holds C(n) = A(n) ∪ B(n), then lim inf A ∪ lim inf B ⊆ lim inf C.

(16) Let X be a non empty 1-sorted structure and A, B, C be sequences of subsets of the carrier of X. If for every natural number n holds C(n) = A(n) ∩ B(n), then lim supC ⊆ lim supA ∩ lim supB.

(17) Let X be a non empty 1-sorted structure, A be a sequence of subsets of the carrier of X, and B be a subset of X. If for every natural number n holds A(n) = B, then lim supA = B.

(18) Let X be a non empty 1-sorted structure, A be a sequence of subsets of the carrier of X, and B be a subset of X. If for every natural number n holds A(n) = B, then lim inf A = B.

(19) Let X be a non empty 1-sorted structure, A, B be sequences of subsets of the carrier of X, and C be a subset of X. If for every natural number n holds B(n) = C−. A(n), then C−. lim inf A ⊆ lim supB.

(20) Let X be a non empty 1-sorted structure, A, B be sequences of subsets of the carrier of X, and C be a subset of X. If for every natural number n holds B(n) = C−. A(n), then C−. lim supA ⊆ lim supB.

3. Ascending and Descending Families of Subsets

Let T be a non empty 1-sorted structure and let S be a sequence of subsets of T. We say that S is descending if and only if:

(Def. 5) For every natural number i holds S(i + 1) ⊆ S(i).

We say that S is ascending if and only if: (Def. 6) For every natural number i holds S(i) ⊆ S(i + 1).

Next we state several propositions:

(21) Let f be a function. Suppose that for every natural number i holds f(i + 1) ⊆ f(i). Let i, j be natural numbers. If i j, then f(j) ⊆ f(i).

(22) Let T be a non empty 1-sorted structure and C be a sequence of subsets of T. Suppose C is descending. Let i, m be natural numbers. If i m, then C(i) ⊆ C(m).

(23) Let T be a non empty 1-sorted structure and C be a sequence of subsets of T. Suppose C is ascending. Let i, m be natural numbers. If i m, then C(m) ⊆ C(i).

(24) Let T be a non empty 1-sorted structure, F be a sequence of subsets of T, and x be a set. Suppose F is descending and there exists a natural number k such that for every natural number n such that n > k holds x ∈ F (n). Then x ∈ ⋂ F.

(25) Let T be a non empty 1-sorted structure and F be a sequence of subsets of T. If F is descending, then lim inf F = ⋂ F.

(26) Let T be a non empty 1-sorted structure and F be a sequence of subsets of T. If F is ascending, then lim supF = ⋃ F.

4. Constant and Convergent Sequences

Let T be a non empty 1-sorted structure and let S be a sequence of subsets of T. We say that S is convergent if and only if:

(Def. 7) lim supS = lim inf S.

We now state the proposition

(27) Let T be a non empty 1-sorted structure and S be a sequence of subsets

of T. If S is constant, then the value of S is a subset of T. Let T be a non empty 1-sorted structure and let S be a sequence of subsets

of T. Let us observe that S is constant if and only if:

(Def. 8) There exists a subset A of T such that for every natural number n holds

S(n) = A. Let T be a non empty 1-sorted structure. Observe that every sequence of

subsets of T which is constant is also convergent, ascending, and descending.

Let T be a non empty 1-sorted structure. Note that there exists a sequence of subsets of T which is constant and non empty.

Let T be a non empty 1-sorted structure and let S be a convergent sequence of subsets of T. The functor limes S yields a subset of T and is defined as follows:

(Def. 9) limes S = lim supS and limes S = lim inf S.

One can prove the following proposition

(28) Let X be a non empty 1-sorted structure, F be a convergent sequence of subsets of X, and x be a set. Then x ∈ limes F if and only if there exists a natural number n such that for every natural number k holds x ∈ F (n + k).

5. Topological Lemmas

In the sequel n denotes a natural number. Let f be a finite sequence of elements of the carrier of E_{T}^{2}. One can check

that L̃(f) is closed.

We now state several propositions:

(29) Let r be a real number, M be a non empty Reflexive metric structure, and x be an element of M. If 0 < r, then x ∈ Ball(x, r).

(30) For every point x of E^{n} and for every real number r holds Ball(x, r) is an open subset of E_{T}^{n}.

(31) For all points p, q of E_{T}^{n} and for all points p′, q′ of E^{n} such that p = p′ and q = q′ holds ρ(p′, q′) = |p − q|.

(32) Let p be a point of E^{n}, x, p′ be points of E_{T}^{n}, and r be a real number. If p = p′ and x ∈ Ball(p, r), then |x − p′| < r.

(33) Let p be a point of E^{n}, x, p′ be points of E_{T}^{n}, and r be a real number. If p = p′ and |x − p′| < r, then x ∈ Ball(p, r).

(34) Let n be a natural number, r be a point of E_{T}^{n}, and X be a subset of E_{T}^{n}. Suppose r ∈ \overline{X}. Then there exists a sequence s_{1} in E_{T}^{n} such that rngs_{1} ⊆ X and s_{1} is convergent and lims_{1} = r.

Let M be a non empty metric space. Note that M_{top} is first-countable. Let n be a natural number. Note that E_{T}^{n} is first-countable. Next we state several propositions:

(35) Let p be a point of E^{n}, q be a point of E_{T}^{n}, and r be a real number. If p = q and r > 0, then Ball(p, r) is a neighbourhood of q.

(36) Let A be a subset of E_{T}^{n}, p be a point of E_{T}^{n}, and p′ be a point of E^{n}. Suppose p = p′. Then p ∈ \overline{A} if and only if for every real number r such that r > 0 holds Ball(p′, r) meets A.

(37) Let x, y be points of E_{T}^{n} and x′ be a point of E^{n}. If x′ = x and x ≠ y, then there exists a real number r such that y ∉ Ball(x′, r).

(38) Let S be a subset of E_{T}^{n}. Then S is non Bounded if and only if for every real number r such that r > 0 there exist points x, y of E^{n} such that x ∈ S and y ∈ S and ρ(x, y) > r.

(39) For all real numbers a, b and for all points x, y of E^{n} such that Ball(x, a) meets Ball(y, b) holds ρ(x, y) < a + b.

(40) Let a, b, c be real numbers and x, y, z be points of E^{n}. If Ball(x, a) meets Ball(z, c) and Ball(z, c) meets Ball(y, b), then ρ(x, y) < a + b + 2 · c.

(41) Let X, Y be non empty topological spaces, x be a point of X, y be a point of Y, and V be a subset of [: X, Y :]. Then V is a neighbourhood of [: {x}, {y}:] if and only if V is a neighbourhood of ⟨⟨x, y⟩⟩.

Now we present two schemes. The scheme TSubsetEx deals with a non empty topological structure A and a unary predicate P, and states that:

There exists a subset X of A such that for every point x of A holds x ∈ X iff P[x]

for all values of the parameters.

The scheme TSubsetUniq deals with a topological structure A and a unary predicate P, and states that:

Let A_{1}, A_{2} be subsets of A. Suppose for every point x of A holds x ∈ A_{1} iff P[x] and for every point x of A holds x ∈ A_{2} iff P[x]. Then A_{1} = A_{2}

for all values of the parameters.

Let T be a non empty topological structure, let S be a sequence of subsets of the carrier of T, and let i be a natural number. Then S(i) is a subset of T.

One can prove the following two propositions:

(42) Let T be a non empty 1-sorted structure, S be a sequence of subsets of the carrier of T, and R be a sequence of naturals. Then S · R is a sequence of subsets of T.

(43) id_{ℕ} is an increasing sequence of naturals.

Let us observe that id_{ℕ} is real-yielding.

6. Subsequences

Let T be a non empty 1-sorted structure and let S be a sequence of subsets of the carrier of T. A sequence of subsets of T is said to be a subsequence of S if:

(Def. 10) There exists an increasing sequence N_{1} of naturals such that it = S · N_{1}.

We now state several propositions:

(44) For every non empty 1-sorted structure T holds every sequence S of subsets of the carrier of T is a subsequence of S.

(45) Let T be a non empty 1-sorted structure, S be a sequence of subsets of T, and S_{1} be a subsequence of S. Then rngS_{1} ⊆ rngS.

(46) Let T be a non empty 1-sorted structure, S_{1} be a sequence of subsets of the carrier of T, and S_{2} be a subsequence of S_{1}. Then every subsequence of S_{2} is a subsequence of S_{1}.

(47) Let T be a non empty 1-sorted structure, F, G be sequences of subsets of the carrier of T, and A be a subset of T. Suppose G is a subsequence of F and for every natural number i holds F (i) = A. Then G = F.

(48) Let T be a non empty 1-sorted structure, A be a constant sequence of subsets of T, and B be a subsequence of A. Then A = B.

(49) Let T be a non empty 1-sorted structure, S be a sequence of subsets of the carrier of T, R be a subsequence of S, and n be a natural number. Then there exists a natural number m such that m n and R(n) = S(m).

Let T be a non empty 1-sorted structure and let X be a constant sequence of subsets of T. Note that every subsequence of X is constant.

The scheme SubSeqChoice deals with a non empty topological space A, a sequence B of subsets of the carrier of A, and a unary predicate P, and states that:

There exists a subsequence S_{1} of B such that for every natural number n holds P[S_{1}(n)]

provided the following condition is satisfied:

• For every natural number n there exists a natural number m such that n m and P[B(m)].

7. The Lower Topological Limit

Let T be a non empty topological space and let S be a sequence of subsets of the carrier of T. The functor Li S yielding a subset of T is defined by the condition (Def. 11).

(Def. 11) Let p be a point of T. Then p ∈ Li S if and only if for every neighbourhood G of p there exists a natural number k such that for every natural number m such that m > k holds S(m) meets G.

The following propositions are true:

(50) Let S be a sequence of subsets of the carrier of E_{T}^{n}, p be a point of E_{T}^{n}, and p′ be a point of E^{n}. Suppose p = p′. Then p ∈ Li S if and only if for every real number r such that r > 0 there exists a natural number k such that for every natural number m such that m > k holds S(m) meets Ball(p′, r).

(51) For every non empty topological space T and for every sequence S of subsets of the carrier of T holds \overline{Li S} = Li S.

(52) For every non empty topological space T and for every sequence S of subsets of the carrier of T holds Li S is closed.

(53) Let T be a non empty topological space and R, S be sequences of subsets of the carrier of T. If R is a subsequence of S, then Li S ⊆ Li R.

(54) Let T be a non empty topological space and A, B be sequences of subsets of the carrier of T. If for every natural number i holds A(i) ⊆ B(i), then Li A ⊆ Li B.

(55) Let T be a non empty topological space and A, B, C be sequences of subsets of the carrier of T. If for every natural number i holds C(i) = A(i) ∪ B(i), then Li A ∪ Li B ⊆ Li C.

(56) Let T be a non empty topological space and A, B, C be sequences of subsets of the carrier of T. If for every natural number i holds C(i) = A(i) ∩ B(i), then Li C ⊆ Li A ∩ Li B.

(57) Let T be a non empty topological space and F, G be sequences of subsets of the carrier of T. If for every natural number i holds G(i) = \overline{F (i)}, then Li G = Li F.

(58) Let S be a sequence of subsets of the carrier of E_{T}^{n} and p be a point of E_{T}^{n}. Given a sequence s in E_{T}^{n} such that s is convergent and for every natural number x holds s(x) ∈ S(x) and p = lims. Then p ∈ Li S.

(59) Let T be a non empty topological space, P be a subset of T, and s be a sequence of subsets of the carrier of T. If for every natural number i holds s(i) ⊆ P, then Li s ⊆ \overline{P} .

(60) Let T be a non empty topological space, F be a sequence of subsets of the carrier of T, and A be a subset of T. If for every natural number i holds F (i) = A, then Li F = \overline{A}.

(61) Let T be a non empty topological space, F be a sequence of subsets of the carrier of T, and A be a closed subset of T. If for every natural number i holds F (i) = A, then Li F = A.

(62) Let S be a sequence of subsets of the carrier of E_{T}^{n} and P be a subset of E_{T}^{n}. Suppose P is Bounded and for every natural number i holds S(i) ⊆ P. Then Li S is Bounded.

(63) Let S be a sequence of subsets of the carrier of E_{T}^{2} and P be a subset of E_{T}^{2}. Suppose P is Bounded and for every natural number i holds S(i) ⊆ P and for every natural number i holds S(i) is compact. Then Li S is compact.

(64) Let A, B be sequences of subsets of the carrier of E_{T}^{n} and C be a sequence of subsets of the carrier of [: E_{T}^{n}, E_{T}^{n}:]. If for every natural number i holds

C(i) = [: A(i), B(i) :], then [: Li A, Li B:] = Li C.

(65) For every sequence S of subsets of E_{T}^{2} holds lim inf S ⊆ Li S.

(66) For every simple closed curve C and for every natural number i holds Fr((UBD L̃(Cage(C, i)))^{c}) = L̃(Cage(C, i)).

8. The Upper Topological Limit

Let T be a non empty topological space and let S be a sequence of subsets of the carrier of T. The functor Ls S yields a subset of T and is defined as follows:

(Def. 12) For every set x holds x ∈ Ls S iff there exists a subsequence A of S such

that x ∈ Li A. One can prove the following propositions:

(67) Let N be a natural number, F be a sequence of E_{T}^{N}, x be a point of E_{T}^{N}, and x′ be a point of E^{N}. Suppose x = x′. Then x is a cluster point of F if and only if for every real number r and for every natural number n such that r > 0 there exists a natural number m such that n m and F (m) ∈ Ball(x′, r).

(68) For every non empty topological space T and for every sequence A of subsets of the carrier of T holds Li A ⊆ Ls A.

(69) Let A, B, C be sequences of subsets of the carrier of E_{T}^{2}. Suppose for every natural number i holds A(i) ⊆ B(i) and C is a subsequence of A. Then there exists a subsequence D of B such that for every natural number i holds C(i) ⊆ D(i).

(70) Let A, B, C be sequences of subsets of the carrier of E_{T}^{2}. Suppose for every natural number i holds A(i) ⊆ B(i) and C is a subsequence of B. Then there exists a subsequence D of A such that for every natural number i holds D(i) ⊆ C(i).

(71) Let A, B be sequences of subsets of the carrier of E_{T}^{2}. If for every natural number i holds A(i) ⊆ B(i), then Ls A ⊆ Ls B.

(72) Let A, B, C be sequences of subsets of the carrier of E_{T}^{2}. If for every natural number i holds C(i) = A(i) ∪ B(i), then Ls A ∪ Ls B ⊆ Ls C.

(73) Let A, B, C be sequences of subsets of the carrier of E_{T}^{2}. If for every natural number i holds C(i) = A(i) ∩ B(i), then Ls C ⊆ Ls A ∩ Ls B.

(74) Let A, B be sequences of subsets of the carrier of E_{T}^{2} and C, C_{1} be sequences of subsets of the carrier of [: E_{T}^{2}, E_{T}^{2} :]. Suppose for every natural number i holds C(i) = [: A(i), B(i) :] and C_{1} is a subsequence of C. Then there exist sequences A_{1}, B_{1} of subsets of the carrier of E_{T}^{2} such that A_{1} is a subsequence of A and B_{1} is a subsequence of B and for every natural number i holds C_{1}(i) = [: A_{1}(i), B_{1}(i) :].

408 adam grabowski

(75) Let A, B be sequences of subsets of the carrier of E_{T}^{2} and C be a sequence of subsets of the carrier of [: E_{T}^{2}, E_{T}^{2} :]. If for every natural number i holds C(i) = [: A(i), B(i) :], then Ls C ⊆ [: Ls A, Ls B:].

(76) Let T be a non empty topological space, F be a sequence of subsets of the carrier of T, and A be a subset of T. If for every natural number i holds F (i) = A, then Li F = Ls F.

(77) Let F be a sequence of subsets of the carrier of E_{T}^{2} and A be a subset of E_{T}^{2}. If for every natural number i holds F (i) = A, then Ls F = \overline{A}.

(78) Let F, G be sequences of subsets of the carrier of E_{T}^{2}. If for every natural number i holds G(i) = \overline{F (i)}, then Ls G = Ls F.

References

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

[2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.

[3] Grzegorz Bancerek. Cartesian product of functions. Formalized Mathematics, 2(4):547– 552, 1991.

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

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

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

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

[8] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990.

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

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

[11] Czesław Byliński and Mariusz Żynel. Cages - the external approximation of Jordan’s curve. Formalized Mathematics, 9(1):19–24, 2001.

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

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

[14] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Arcs, line segments and special polygonal arcs. Formalized Mathematics, 2(5):617–621, 1991.

[15] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Simple closed curves. Formalized Mathematics, 2(5):663–664, 1991.

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

[17] Jarosław Kotowicz. Monotone real sequences. Subsequences. Formalized Mathematics, 1(3):471–475, 1990.

[18] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269–272, 1990.

[19] Kazimierz Kuratowski. Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.

[20] Yatsuka Nakamura, Andrzej Trybulec, and Czesław Byliński. Bounded domains and unbounded domains. Formalized Mathematics, 8(1):1–13, 1999.

[21] Andrzej Nędzusiak. σ-fields and probability. Formalized Mathematics, 1(2):401–407, 1990.

[22] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990.

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

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

on the kuratowski limit operators 409

[25] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111–115, 1991.

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

[27] Bartłomiej Skorulski. First-countable, sequential, and Frechet spaces. Formalized Mathematics, 7(1):81–86, 1998.

[28] Bartłomiej Skorulski. The sequential closure operator in sequential and Frechet spaces. Formalized Mathematics, 8(1):47–54, 1999.

[29] Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics.

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

[31] Andrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4):535–545, 1991.

[32] Andrzej Trybulec. Moore-Smith convergence. Formalized Mathematics, 6(2):213–225, 1997.

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

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

[35] Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231–237, 1990.

On the Segmentation of a Simple Closed Curve^{1}

Andrzej Trybulec University of Białystok

Summary. The main goal of the work was to introduce the concept of the segmentation of a simple closed curve into (arbitrary small) arcs. The existence of it has been proved by Yatsuka Nakamura [21]. The concept of the gap of a segmentation is also introduced. It is the smallest distance between disjoint segments in the segmentation. For this purpose, the relationship between segments of an arc [24] and segments on a simple closed curve [21] has been shown.

MML Identifier: JORDAN A.

The papers [30], [35], [10], [3], [2], [29], [1], [13], [8], [9], [7], [4], [34], [25], [33], [22], [20], [28], [15], [26], [27], [18], [6], [12], [31], [19], [14], [16], [17], [23], [5], [24], [21], [11], and [32] provide the notation and terminology for this paper.

1. Preliminaries

The scheme AndScheme deals with a non empty set A and two unary predicates P, Q, and states that:

{a; a ranges over elements of A : P[a] ∧ Q[a]} = {a_{1}; a_{1} ranges

over elements of A : P[a_{1}]} ∩ {a_{2}; a_{2} ranges over elements of A :
Q[a_{2}]}

for all values of the parameters.

For simplicity, we follow the rules: C is a simple closed curve, p, q are points of E_{T}^{2}, i, j, k, n are natural numbers, and e is a real number.

The following proposition is true (1) For all finite non empty subsets A, B of ℝ holds min(A ∪ B) =

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

min(minA, minB). Let T be a non empty topological space. One can check that there exists a

subset of T which is compact and non empty. Next we state several propositions:

(2) Let T be a non empty topological space, f be a continuous real map of T, and A be a compact subset of T. Then f^{∘}A is compact.

(3) For every compact subset A of ℝ and for every non empty subset B of ℝ such that B ⊆ A holds inf B ∈ A.

(4) Let A, B be compact non empty subsets of E_{T}^{n}, f be a continuous real map of [: E_{T}^{n}, E_{T}^{n}:], and g be a real map of E_{T}^{n}. Suppose that for every point p of E_{T}^{n} there exists a subset G of ℝ such that G = {f(p, q); q ranges over points of E_{T}^{n}: q ∈ B} and g(p) = inf G. Then inf(f^{∘}[: A, B:]) = inf(g^{∘}A).

(5) Let A, B be compact non empty subsets of E_{T}^{n}, f be a continuous real map of [: E_{T}^{n}, E_{T}^{n}:], and g be a real map of E_{T}^{n}. Suppose that for every point q of E_{T}^{n} there exists a subset G of ℝ such that G = {f(p, q); p ranges over points of E_{T}^{n}: p ∈ A} and g(q) = inf G. Then inf(f^{∘}[: A, B:]) = inf(g^{∘}B).

(6) If q ∈ LowerArc(C) and q ≠ W_{min}(C), then E_{max}(C) _{C} q.

(7) If q ∈ UpperArc(C), then q _{C} E_{max}(C).

2. The Euclidean Distance

Let us consider n. The functor EuclDist(n) yielding a real map of [: E_{T}^{n}, E_{T}^{n}:] is defined as follows:

(Def. 1) For all points p, q of E_{T}^{n} holds (EuclDist(n))(p, q) = |p − q|.

Let T be a non empty topological space and let f be a real map of T. Let us observe that f is continuous if and only if:

(Def. 2) For every point p of T and for every neighbourhood N of f(p) there

exists a neighbourhood V of p such that f^{∘}V ⊆ N. Let us consider n. Note that EuclDist(n) is continuous.

3. On the Distance between Subsets of a Euclidean Space

The following proposition is true

(8) For all non empty compact subsets A, B of E_{T}^{n} such that A misses B holds dist_{min}(A, B) > 0.

4. On the Segments

The following propositions are true:

(9) If p _{C} q and q _{C} E_{max}(C) and p ≠ q, then Segment(p, q, C) = Segment(UpperArc(C), W_{min}(C), E_{max}(C), p, q).

(10) If E_{max}(C) _{C} q, then Segment(E_{max}(C), q, C) = Segment(LowerArc(C), E_{max}(C), W_{min}(C), E_{max}(C), q).

(11) If E_{max}(C) _{C} q, then Segment(q, W_{min}(C), C) = Segment(LowerArc(C), E_{max}(C), W_{min}(C), q, W_{min}(C)).

(12) If p _{C} q and E_{max}(C) _{C} p, then Segment(p, q, C) = Segment(LowerArc(C), E_{max}(C), W_{min}(C), p, q).

(13) If p _{C} E_{max}(C) and E_{max}(C) _{C} q, then Segment(p, q, C) = RSegment(UpperArc(C), W_{min}(C), E_{max}(C), p)∪LSegment(LowerArc(C), E_{max}(C), W_{min}(C), q).

(14) If p _{C} E_{max}(C), then Segment(p, W_{min}(C), C) = RSegment(UpperArc (C), W_{min}(C), E_{max}(C), p) ∪ LSegment(LowerArc(C), E_{max}(C), W_{min}(C), W_{min}(C)).

(15) RSegment(UpperArc(C), W_{min}(C), E_{max}(C), p) = Segment(UpperArc (C), W_{min}(C), E_{max}(C), p, E_{max}(C)).

(16) LSegment(LowerArc(C), E_{max}(C), W_{min}(C), p) = Segment(LowerArc(C), E_{max}(C), W_{min}(C), E_{max}(C), p).

(17) For every point p of E_{T}^{2} such that p ∈ C and p ≠ W_{min}(C) holds Segment(p, W_{min}(C), C) is an arc from p to W_{min}(C).

(18) For all points p, q of E_{T}^{2} such that p ≠ q and p _{C} q holds Segment(p, q, C) is an arc from p to q.

(19) C = Segment(W_{min}(C), W_{min}(C), C).

(20) For every point q of E_{T}^{2} such that q ∈ C holds Segment(q, W_{min}(C), C) is compact.

(21) For all points q_{1}, q_{2} of E_{T}^{2} such that q_{1} _{C} q_{2} holds Segment(q_{1}, q_{2}, C) is compact.

5. The Concept of a Segmentation

Let us consider C. A finite sequence of elements of E_{T}^{2} is said to be a segmentation of C if it satisfies the conditions (Def. 3).

(Def. 3) It_{1} = W_{min}(C) and it is one-to-one and 8 lenit and rngit ⊆ C and for every natural number i such that 1 i and i < lenit holds it_{i} _{C} it_{i+1} and for every natural number i such that 1 i and i + 1 < lenit holds Segment(it_{i}, it_{i+1}, C) ∩ Segment(it_{i+1}, it_{i+2}, C) = {it_{i+1}} and Segment(it_{len it}, it_{1}, C) ∩ Segment(it_{1}, it_{2}, C) = {it_{1}} and Segment(it_{len it− ′1}, it_{len it}, C) ∩ Segment(it_{len it}, it_{1}, C) = {it_{len it}} and Segment(it_{len it− ′1}, it_{len it}, C) misses Segment(it_{1}, it_{2}, C) and for all natural numbers i, j such that 1 i and i < j and j < lenit and i and j are not adjacent holds Segment(it_{i}, it_{i+1}, C) misses Segment(it_{j}, it_{j+1}, C) and for every natural number i such that 1 < i and i + 1 < lenit holds Segment(it_{len it}, it_{1}, C) misses Segment(it_{i}, it_{i+1}, C).

Let us consider C. One can verify that every segmentation of C is non trivial. One can prove the following proposition

(22) For every segmentation S of C and for every i such that 1 i and i lenS holds S_{i} ∈ C.

6. The Segments of a Segmentation

Let us consider C, let i be a natural number, and let S be a segmentation of C. The functor Segm(S, i) yields a subset of E_{T}^{2} and is defined by:

(Def. 4) Segm(S, i) = \{ \begin{matrix}Segment(S_{i}, S_{i+1}, C), if 1 i and i < lenS, \\ Segment(S_{len S}, S_{1}, C), otherwise. \end{matrix}

The following proposition is true

(23) For every segmentation S of C such that i ∈ domS holds Segm(S, i) ⊆ C. Let us consider C, let S be a segmentation of C, and let us consider i. Note

that Segm(S, i) is non empty and compact.

We now state several propositions:

(24) For every segmentation S of C and for every p such that p ∈ C there exists a natural number i such that i ∈ domS and p ∈ Segm(S, i).

(25) Let S be a segmentation of C and given i, j. Suppose 1 i and i < j and j < lenS and i and j are not adjacent. Then Segm(S, i) misses Segm(S, j).

(26) For every segmentation S of C and for every j such that 1 < j and j < lenS − ′1 holds Segm(S, lenS) misses Segm(S, j).

(27) Let S be a segmentation of C and given i, j. Suppose 1 i and i < j and j < lenS and i and j are adjacent. Then Segm(S, i)∩Segm(S, j) = {S_{i+1}}.

(28) Let S be a segmentation of C and given i, j. Suppose 1 i and i < j and j < lenS and i and j are adjacent. Then Segm(S, i) meets Segm(S, j).

(29) For every segmentation S of C holds Segm(S, lenS)∩Segm(S, 1) = {S_{1}}.

(30) For every segmentation S of C holds Segm(S, lenS) meets Segm(S, 1).

(31) For every segmentation S of C holds Segm(S, lenS) ∩ Segm(S, lenS − ′ 1) = {S_{len S}}.

(32) For every segmentation S of C holds Segm(S, lenS) meets Segm(S, lenS − ′1).

7. The Diameter of a Segmentation

Let us consider n and let C be a subset of E_{T}^{n}. The functor ØC yielding a real number is defined by:

(Def. 5) There exists a subset W of E^{n} such that W = C and ØC = ØW.

Let us consider C and let S be a segmentation of C. The functor ØS yielding a real number is defined as follows:

(Def. 6) There exists a non empty finite subset S_{1} of ℝ such that S_{1} =

{Ø Segm(S, i) : i ∈ domS} and ØS = maxS_{1}. We now state three propositions:

(33) For every segmentation S of C and for every i holds Ø Segm(S, i) ØS.

(34) For every segmentation S of C and for every real number e such that for every i holds Ø Segm(S, i) < e holds ØS < e.

(35) For every real number e such that e > 0 there exists a segmentation S of C such that ØS < e.

8. The Concept of the Gap of a Segmentation

Let us consider C and let S be a segmentation of C. The functor Gap(S) yields a real number and is defined by the condition (Def. 7).

(Def. 7) There exist non empty finite subsets S_{1}, S_{2} of ℝ such that S_{1} = {dist_{min}(Segm(S, i), Segm(S, j)) : 1 i ∧ i < j ∧ j < lenS ∧ i and j are not adjacent} and S_{2} = {dist_{min}(Segm(S, lenS), Segm(S, k)) : 1 < k ∧ k < lenS − ′1} and Gap(S) = min(minS_{1}, minS_{2}).

Next we state two propositions:

(36) Let S be a segmentation of C. Then there exists a finite non empty subset F of ℝ such that F = {dist_{min}(Segm(S, i), Segm(S, j)) : 1 i ∧ i < j ∧ j lenS ∧ Segm(S, i) misses Segm(S, j)} and Gap(S) = minF.

(37) For every segmentation S of C holds Gap(S) > 0.

References

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

[2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.

[3] Grzegorz Bancerek. Sequences of ordinal numbers. Formalized Mathematics, 1(2):281– 290, 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 and Yatsuka Nakamura. The theorem of Weierstrass. Formalized Mathematics, 5(3):353–359, 1996.

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

416 andrzej trybulec

[7] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 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] Czesław Byliński and Piotr Rudnicki. Bounding boxes for compact sets in E^{2}. Formalized Mathematics, 6(3):427–440, 1997.

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

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

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

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

[16] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Arcs, line segments and special polygonal arcs. Formalized Mathematics, 2(5):617–621, 1991.

[17] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Simple closed curves. Formalized Mathematics, 2(5):663–664, 1991.

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

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

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

[21] Yatsuka Nakamura. On the dividing function of the simple closed curve into segments. Formalized Mathematics, 7(1):135–138, 1998.

[22] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Formalized Mathematics, 5(2):167–172, 1996.

[23] Yatsuka Nakamura and Andrzej Trybulec. Adjacency concept for pairs of natural numbers. Formalized Mathematics, 6(1):1–3, 1997.

[24] Yatsuka Nakamura and Andrzej Trybulec. A decomposition of a simple closed curves and the order of their points. Formalized Mathematics, 6(4):563–572, 1997.

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

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

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

[28] Konrad Raczkowski and Paweł Sadowski. Topological properties of subsets in real numbers. Formalized Mathematics, 1(4):777–780, 1990.

[29] Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics.

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

[31] Andrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4):535–545, 1991.

[32] Andrzej Trybulec. On the minimal distance between sets in Euclidean space. Formalized Mathematics, 10(3):153–158, 2002.

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

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

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

On the Calculus of Binary Arithmetics

Shunichi Kobayashi University of Matsumoto

Summary. In this paper, we have binary arithmetic and its related operations. We include some theorems concerning logical operators.

MML Identifier: BINARI 5.

The notation and terminology used in this paper have been introduced in the following articles: [3], [4], [2], and [1].

Let x, y be boolean sets. The functor x ′nand′ y is defined as follows: (Def. 1) x ′nand′ y = ¬(x ∧ y).

Let us note that the functor x ′nand′ y is commutative.

Let x, y be boolean sets. Note that x ′nand′ y is boolean. Let x, y be elements of Boolean. Then x ′nand′ y is an element of Boolean. Let x, y be boolean sets. The functor x ′nor′ y is defined by:

(Def. 2) x ′nor′ y = ¬(x ∨ y).

Let us note that the functor x ′nor′ y is commutative.

Let x, y be boolean sets. Note that x ′nor′ y is boolean. Let x, y be elements of Boolean. Then x ′nor′ y is an element of Boolean. Let x, y be boolean sets. The functor x ′xnor′ y is defined as follows:

(Def. 3) x ′xnor′ y = ¬(x ⊕ y).

Let us observe that the functor x ′xnor′ y is commutative.

Let x, y be boolean sets. Note that x ′xnor′ y is boolean. Let x, y be elements of Boolean. Then x ′xnor′ y is an element of Boolean. In the sequel x, y, z, w are boolean sets. The following propositions are true:

(1) true ′nand′ x = ¬x.

(2) false ′nand′ x = true.

(3) x ′nand′ x = ¬x and ¬(x ′nand′ x) = x.

(4) ¬(x ′nand′ y) = x ∧ y.

(5) x ′nand′ ¬x = true and ¬(x ′nand′ ¬x) = false.

(6) x ′nand′ y ∧ z = ¬(x ∧ y ∧ z).

(7) x ′nand′ y ∧ z = x ∧ y ′nand′ z.

(8) x ′nand′ (y ∨ z) = ¬(x ∧ y) ∧ ¬(x ∧ z).

(9) x ′nand′ (y ⊕ z) = x ∧ y ⇔ x ∧ z.

(10) true ′nor′ x = false.

(11) false ′nor′ x = ¬x.

(12) x ′nor′ x = ¬x and ¬(x ′nor′ x) = x.

(13) ¬(x ′nor′ y) = x ∨ y.

(14) x ′nor′ ¬x = false and ¬(x ′nor′ ¬x) = true.

(15) x ′nor′ y ∧ z = ¬(x ∨ y) ∨ ¬(x ∨ z).

(16) x ′nor′ (y ∨ z) = ¬(x ∨ y ∨ z).

(17) true ′xnor′ x = x.

(18) false ′xnor′ x = ¬x.

(19) x ′xnor′ x = true and ¬(x ′xnor′ x) = false.

(20) ¬(x ′xnor′ y) = x ⊕ y.

(21) x ′xnor′ ¬x = false and ¬(x ′xnor′ ¬x) = true.

(22) x ⋐ y ⇒ z iff x ∧ y ⋐ z.

(23) x ⇔ y = (x ⇒ y) ∧ (y ⇒ x).

(24) x ⇔ y = true iff x ⇒ y = true and y ⇒ x = true.

(25) If x ⇒ y = true and y ⇒ x = true, then x = y.

(26) If x ⇒ y = true and y ⇒ z = true, then x ⇒ z = true.

(27) If x ⇔ y = true and y ⇔ z = true, then x ⇔ z = true.

(28) x ⇒ y = ¬y ⇒ ¬x.

(29) x ⇔ y = ¬x ⇔ ¬y.

(30) If x ⇔ y = true and z ⇔ w = true, then x ∧ z ⇔ y ∧ w = true.

(31) If x ⇔ y = true and z ⇔ w = true, then x ⇒ z ⇔ y ⇒ w = true.

(32) If x ⇔ y = true and z ⇔ w = true, then x ∨ z ⇔ y ∨ w = true.

(33) If x ⇔ y = true and z ⇔ w = true, then x ⇔ z ⇔ y ⇔ w = true.

(34) If x = true and x ⇒ y = true, then y = true.

(35) If y = true, then x ⇒ y = true.

(36) If ¬x = true, then x ⇒ y = true.

(37) x ⇒ x = true.

(38) If x ⇒ y = true and x ⇒ ¬y = true, then ¬x = true.

(39) ¬x ⇒ x ⇒ x = true.

(40) x ⇒ y ⇒ ¬(y ∧ z) ⇒ ¬(x ∧ z) = true.

(41) x ⇒ y ⇒ y ⇒ z ⇒ x ⇒ z = true.

(42) If x ⇒ y = true, then y ⇒ z ⇒ x ⇒ z = true.

(43) y ⇒ x ⇒ y = true.

(44) x ⇒ y ⇒ z ⇒ y ⇒ z = true.

(45) y ⇒ y ⇒ x ⇒ x = true.

(46) z ⇒ y ⇒ x ⇒ y ⇒ z ⇒ x = true.

(47) y ⇒ z ⇒ x ⇒ y ⇒ x ⇒ z = true.

(48) y ⇒ y ⇒ z ⇒ y ⇒ z = true.

(49) x ⇒ y ⇒ z ⇒ x ⇒ y ⇒ x ⇒ z = true.

(50) If x = true, then x ⇒ y ⇒ y = true.

(51) If z ⇒ y ⇒ x = true, then y ⇒ z ⇒ x = true.

(52) If z ⇒ y ⇒ x = true and y = true, then z ⇒ x = true.

(53) If z ⇒ y ⇒ x = true and y = true and z = true, then x = true.

(54) If y ⇒ y ⇒ z = true, then y ⇒ z = true.

(55) If x ⇒ y ⇒ z = true, then x ⇒ y ⇒ x ⇒ z = true.

Acknowledgments

This research was partially supported by the research funds of the University of Matsumoto.

References

[1] Shunichi Kobayashi and Kui Jia. A theory of Boolean valued functions and partitions. Formalized Mathematics, 7(2):249–254, 1998.

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

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

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

SCMPDS Is Not Standard

Artur Korniłowicz^{1} University of Białystok Yasunari Shidama Shinshu University Nagano

Summary. The aim of the paper is to show that SCMPDS ([8]) does not belong to the class of standard computers ([16]).

MML Identifier: SCMPDS 9.

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

1. Preliminaries

In this paper r, s are real numbers. We now state several propositions:

(1) 0 r + |r|.

(2) 0 − r + |r|.

(3) If |r| = |s|, then r = s or r = − s.

(4) For all natural numbers i, j such that i < j and i ≠ 0 holds \frac{i}{j} is not integer.

(5) {2 · k; k ranges over natural numbers: k > 1} is infinite.

(6) For every function f and for all sets a, b, c such that a ≠ c holds (f+·(a⟼→ . b))(c) = f(c).

(7) For every function f and for all sets a, b, c, d such that a ≠ b holds (f+·[a ⟼→ c, b ⟼→ d])(a) = c and (f+·[a ⟼→ c, b ⟼→ d])(b) = d.

1This paper was written during the first author’s post-doctoral fellowship granted by Shinshu University, Japan.

2. SCMPDS

For simplicity, we adopt the following rules: a, b are Int positions, i is an instruction of SCMPDS, l is an instruction-location of SCMPDS, and k, k_{1}, k_{2} are integers.

Let l_{1}, l_{2} be Int positions and let a, b be integers. Then [l_{1} ⟼→ a, l_{2} ⟼→ b] is a finite partial state of SCMPDS.

One can verify that SCMPDS has non trivial instruction locations.

Let l be an instruction-location of SCMPDS. The functor locnum(l) yields a natural number and is defined by:

(Def. 1) i_{locnum(l)} = l.

Let l be an instruction-location of SCMPDS. Then locnum(l) is an element of ℕ.

We now state a number of propositions:

(8) l = 2 · locnum(l) + 2.

(9) For all instruction-locations l_{3}, l_{4} of SCMPDS such that l_{3} ≠ l_{4} holds locnum(l_{3}) ≠ locnum(l_{4}).

(10) For all instruction-locations l_{3}, l_{4} of SCMPDS such that l_{3} ≠ l_{4} holds Next(l_{3}) ≠ Next(l_{4}).

(11) Let N be a set with non empty elements, S be an IC-Ins-separated definite non empty non void AMI over N, i be an instruction of S, and l be an instruction-location of S. Then JUMP(i) ⊆ NIC(i, l).

(12) If for every state s of SCMPDS such that IC_{s} = l and s(l) = i holds (Exec(i, s))(IC_{SCMPDS} ) = Next(IC_{s}), then NIC(i, l) = {Next(l)}.

(13) If for every instruction-location l of SCMPDS holds NIC(i, l) = {Next(l)}, then JUMP(i) is empty.

(14) NIC(goto k, l) = {2 · |k + locnum(l)| + 2}.

(15) NIC(returna, l) = {2 · k; k ranges over natural numbers: k > 1}.

(16) NIC(saveIC(a, k_{1}), l) = {Next(l)}.

(17) NIC(a:=k_{1}, l) = {Next(l)}.

(18) NIC(a_{k_{1}}:=k_{2}, l) = {Next(l)}.

(19) NIC((a, k_{1}) := (b, k_{2}), l) = {Next(l)}.

(20) NIC(AddTo(a, k_{1}, k_{2}), l) = {Next(l)}.

(21) NIC(AddTo(a, k_{1}, b, k_{2}), l) = {Next(l)}.

(22) NIC(SubFrom(a, k_{1}, b, k_{2}), l) = {Next(l)}.

(23) NIC(MultBy(a, k_{1}, b, k_{2}), l) = {Next(l)}.

(24) NIC(Divide(a, k_{1}, b, k_{2}), l) = {Next(l)}.

(25) NIC((a, k_{1}) <> 0 goto k_{2}, l) = {Next(l), |2 · (k_{2} + locnum(l))| + 2}.

(26) NIC((a, k_{1}) <= 0 goto k_{2}, l) = {Next(l), |2 · (k_{2} + locnum(l))| + 2}.

(27) NIC((a, k_{1}) >= 0 goto k_{2}, l) = {Next(l), |2 · (k_{2} + locnum(l))| + 2}. Let us consider k. Observe that JUMP(goto k) is empty. Next we state the proposition

(28) JUMP(returna) = {2 · k; k ranges over natural numbers: k > 1}. Let us consider a. Note that JUMP(returna) is infinite. Let us consider a, k_{1}. One can verify that JUMP(saveIC(a, k_{1})) is empty. Let us consider a, k_{1}. Observe that JUMP(a:=k_{1}) is empty. Let us consider a, k_{1}, k_{2}. Note that JUMP(a_{k_{1}}:=k_{2}) is empty. Let us consider a, b, k_{1}, k_{2}. One can check that JUMP((a, k_{1}) := (b, k_{2})) is

empty.

Let us consider a, k_{1}, k_{2}. One can verify that JUMP(AddTo(a, k_{1}, k_{2})) is empty.

Let us consider a, b, k_{1}, k_{2}. One can verify the following observations:

∗ JUMP(AddTo(a, k_{1}, b, k_{2})) is empty,

∗ JUMP(SubFrom(a, k_{1}, b, k_{2})) is empty,

∗ JUMP(MultBy(a, k_{1}, b, k_{2})) is empty, and

∗ JUMP(Divide(a, k_{1}, b, k_{2})) is empty. Let us consider a, k_{1}, k_{2}. One can verify the following observations:

∗ JUMP((a, k_{1}) <> 0 goto k_{2}) is empty,

∗ JUMP((a, k_{1}) <= 0 goto k_{2}) is empty, and

∗ JUMP((a, k_{1}) >= 0 goto k_{2}) is empty. Next we state two propositions:

(29) SUCC(l) = the instruction locations of SCMPDS.

(30) Let N be a set with non empty elements, S be an IC-Ins-separated definite non empty non void AMI over N, and l_{3}, l_{4} be instruction-locations of S. If SUCC(l_{3}) = the instruction locations of S, then l_{3} l_{4}.

Let us mention that SCMPDS is non InsLoc-antisymmetric. One can verify that SCMPDS is non standard.

References

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

[2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.

[3] Grzegorz Bancerek. Sequences of ordinal numbers. Formalized Mathematics, 1(2):281– 290, 1990.

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

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

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

[7] Czesław Byliński. The modification of a function by a function and the iteration of the composition of a function. Formalized Mathematics, 1(3):521–527, 1990.

424 artur korniłowicz and yasunari shidama

[8] Jing-Chao Chen. The SCMPDS computer and the basic semantics of its instructions. Formalized Mathematics, 8(1):183–191, 1999.

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

[10] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Formalized Mathematics, 3(2):151–160, 1992.

[11] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990.

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

[13] Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics.

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

[15] Andrzej Trybulec and Yatsuka Nakamura. Some remarks on the simple concrete model of computer. Formalized Mathematics, 4(1):51–56, 1993.

[16] Andrzej Trybulec, Piotr Rudnicki, and Artur Korniłowicz. Standard ordering of instruction locations. Formalized Mathematics, 9(2):291–301, 2001.

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

[18] Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821–827, 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.

Received September 27, 2003

On the Upper and Lower Approximations of the Curve^{1}

Robert Milewski University of Białystok

MML Identifier: JORDAN19.

The papers [28], [32], [2], [15], [1], [5], [6], [4], [31], [16], [29], [17], [27], [13], [3], [25], [26], [10], [11], [8], [30], [14], [20], [18], [12], [23], [22], [24], [7], [9], [19], and [21] provide the terminology and notation for this paper.

In this paper n denotes a natural number.

Let C be a simple closed curve. The functor UpperAppr(C) yields a sequence of subsets of the carrier of E_{T}^{2} and is defined as follows:

(Def. 1) For every natural number i holds (UpperAppr(C))(i) =

UpperArc(L̃(Cage(C, i))). The functor LowerAppr(C) yielding a sequence of subsets of the carrier of E_{T}^{2} is defined as follows:

(Def. 2) For every natural number i holds (LowerAppr(C))(i) =

LowerArc(L̃(Cage(C, i))). Let C be a simple closed curve. The functor NorthArc(C) yields a subset of

E_{T}^{2} and is defined by: (Def. 3) NorthArc(C) = Li UpperAppr(C).

The functor SouthArc(C) yielding a subset of E_{T}^{2} is defined as follows: (Def. 4) SouthArc(C) = Li LowerAppr(C).

We now state a number of propositions:

(1) For all natural numbers n, m such that n m and n ≠ 0 holds \frac{n+1}{n} \frac{m+1}{m}.

1This work has been partially supported by the CALCULEMUS grant HPRN-CT-2000-00102.

(2) Let E be a compact non vertical non horizontal subset of E_{T}^{2} and m, j be natural numbers. Suppose 1 m and m n and 1 j and j widthGauge(E, n). Then L(Gauge(E, n) ∘ (CenterGauge(E, n), widthGauge(E, n)), Gauge(E, n) ∘ (CenterGauge(E, n), j)) ⊆ L(Gauge(E, m) ∘ (CenterGauge(E, m), widthGauge(E, m)), Gauge(E, n) ∘ (CenterGauge(E, n), j)).

(3) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j be natural numbers. Suppose 1 i and i lenGauge(C, n) and 1 j and j widthGauge(C, n) and Gauge(C, n)∘(i, j) ∈ L̃(Cage(C, n)). Then L(Gauge(C, n) ∘ (i, widthGauge(C, n)), Gauge(C, n) ∘ (i, j)) meets L̃(UpperSeq(C, n)).

(4) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and n be a natural number. Suppose n > 0. Let i, j be natural numbers. Suppose 1 i and i lenGauge(C, n) and 1 j and j widthGauge(C, n) and Gauge(C, n) ∘ (i, j) ∈ L̃(Cage(C, n)). Then L(Gauge(C, n) ∘ (i, widthGauge(C, n)), Gauge(C, n) ∘ (i, j)) meets UpperArc(L̃(Cage(C, n))).

(5) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and j be a natural number. Suppose Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), j) ∈ LowerArc(L̃(Cage(C, n + 1))) and 1 j and j widthGauge(C, n + 1). Then L(Gauge(C, 1) ∘ (CenterGauge(C, 1), widthGauge(C, 1)), Gauge(C, n + 1) ∘ (CenterGauge (C, n + 1), j)) meets UpperArc(L̃(Cage(C, n + 1))).

(6) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2}, f be a finite sequence of elements of E_{T}^{2}, and k be a natural number. Suppose 1 k and k+1 lenf and f is a sequence which elements belong to Gauge(C, n). Then ρ(f_{k}, f_{k+1}) = \frac{N-bound (C)−S-bound (C)}{2^{n}} or ρ(f_{k}, f_{k+1}) = \frac{E-bound (C)−W-bound (C)}{2^{n}} .

(7) Let M be a symmetric triangle metric structure, r be a real number, and p, q, x be elements of M. If p ∈ Ball(x, r) and q ∈ Ball(x, r), then ρ(p, q) < 2 · r.

(8) Let A be a subset of E_{T}^{n}, p be a point of E_{T}^{n}, and p′ be a point of E^{n}. Suppose p = p′. Let s be a real number. Suppose s > 0. Then p ∈ \overline{A} if and only if for every real number r such that 0 < r and r < s holds Ball(p′, r) meets A.

(9) For every compact connected non vertical non horizontal subset C of E_{T}^{2} holds N-bound(C) < N-bound(L̃(Cage(C, n))).

(10) For every compact connected non vertical non horizontal subset C of E_{T}^{2} holds E-bound(C) < E-bound(L̃(Cage(C, n))).

(11) For every compact connected non vertical non horizontal subset C of E_{T}^{2}

holds S-bound(L̃(Cage(C, n))) < S-bound(C).

(12) For every compact connected non vertical non horizontal subset C of E_{T}^{2} holds W-bound(L̃(Cage(C, n))) < W-bound(C).

(13) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n) and 1 k and k j and j widthGauge(C, n) and L(Gauge(C, n) ∘ (i, k), Gauge(C, n) ∘ (i, j)) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (i, k)} and L(Gauge(C, n) ∘ (i, k), Gauge(C, n) ∘ (i, j)) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (i, j)}. Then L(Gauge(C, n) ∘ (i, k), Gauge(C, n) ∘ (i, j)) meets UpperArc(C).

(14) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n) and 1 k and k j and j widthGauge(C, n) and L(Gauge(C, n) ∘ (i, k), Gauge(C, n) ∘ (i, j)) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (i, k)} and L(Gauge(C, n) ∘ (i, k), Gauge(C, n) ∘ (i, j)) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (i, j)}. Then L(Gauge(C, n) ∘ (i, k), Gauge(C, n) ∘ (i, j)) meets LowerArc(C).

(15) Let C be a simple closed curve and i, j, k be natural numbers. Suppose that 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and n > 0 and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) ∩ LowerArc(L̃(Cage(C, n))) = {Gauge(C, n) ∘ (i, k)} and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) ∩ UpperArc(L̃(Cage(C, n))) = {Gauge(C, n) ∘ (i, j)}. Then L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) meets UpperArc(C).

(16) Let C be a simple closed curve and i, j, k be natural numbers. Suppose that 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and n > 0 and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) ∩ LowerArc(L̃(Cage(C, n))) = {Gauge(C, n) ∘ (i, k)} and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) ∩ UpperArc(L̃(Cage(C, n))) = {Gauge(C, n) ∘ (i, j)}. Then L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) meets LowerArc(C).

(17) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and Gauge(C, n) ∘ (i, k) ∈ L̃(LowerSeq(C, n)) and Gauge(C, n) ∘ (i, j) ∈ L̃(UpperSeq(C, n)). Then L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) meets UpperArc(C).

(18) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and Gauge(C, n) ∘ (i, k) ∈ L̃(LowerSeq(C, n)) and Gauge(C, n) ∘ (i, j) ∈ L̃(UpperSeq(C, n)). Then L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) meets LowerArc(C).

(19) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n) and 1 j

and j  k and k  widthGauge(C, n) and n > 0 and

Gauge(C, n) ∘ (i, k) ∈ LowerArc(L̃(Cage(C, n))) and Gauge(C, n) ∘ (i, j) ∈ UpperArc(L̃(Cage(C, n))). Then L(Gauge(C, n)∘(i, j), Gauge(C, n)∘(i, k)) meets UpperArc(C).

(20) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and n > 0 and Gauge(C, n) ∘ (i, k) ∈ LowerArc(L̃(Cage(C, n))) and Gauge(C, n) ∘ (i, j) ∈ UpperArc(L̃(Cage(C, n))). Then L(Gauge(C, n)∘(i, j), Gauge(C, n)∘(i, k)) meets LowerArc(C).

(21) Let C be a simple closed curve and i_{1}, i_{2}, j, k be natural numbers. Suppose that 1 < i_{1} and i_{1} i_{2} and i_{2} < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(UpperSeq(C, n)) = {Gauge(C, n)∘(i_{1}, j)} and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(LowerSeq(C, n)) = {Gauge(C, n)∘(i_{2}, k)}. Then L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n) ∘ (i_{2}, k)) meets UpperArc(C).

(22) Let C be a simple closed curve and i_{1}, i_{2}, j, k be natural numbers. Suppose that 1 < i_{1} and i_{1} i_{2} and i_{2} < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(UpperSeq(C, n)) = {Gauge(C, n)∘(i_{1}, j)} and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(LowerSeq(C, n)) = {Gauge(C, n)∘(i_{2}, k)}. Then L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n) ∘ (i_{2}, k)) meets LowerArc(C).

(23) Let C be a simple closed curve and i_{1}, i_{2}, j, k be natural numbers. Suppose that 1 < i_{2} and i_{2} i_{1} and i_{1} < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(UpperSeq(C, n)) = {Gauge(C, n)∘(i_{1}, j)} and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(LowerSeq(C, n)) = {Gauge(C, n)∘(i_{2}, k)}. Then L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n) ∘ (i_{2}, k)) meets UpperArc(C).

(24) Let C be a simple closed curve and i_{1}, i_{2}, j, k be natural numbers. Suppose that 1 < i_{2} and i_{2} i_{1} and i_{1} < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(UpperSeq(C, n)) = {Gauge(C, n)∘(i_{1}, j)} and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(LowerSeq(C, n)) = {Gauge(C, n)∘(i_{2}, k)}. Then L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n) ∘ (i_{2}, k)) meets LowerArc(C).

(25) Let C be a simple closed curve and i_{1}, i_{2}, j, k be natural numbers. Suppose that 1 < i_{1} and i_{1} < lenGauge(C, n + 1) and 1 < i_{2} and i_{2} < lenGauge(C, n+1) and 1 j and j k and k widthGauge(C, n+1) and Gauge(C, n+1)∘(i_{1}, k) ∈ LowerArc(L̃(Cage(C, n+1))) and Gauge(C, n+ 1) ∘ (i_{2}, j) ∈ UpperArc(L̃(Cage(C, n + 1))). Then L(Gauge(C, n + 1) ∘ (i_{2}, j), Gauge(C, n + 1) ∘ (i_{2}, k)) ∪ L(Gauge(C, n + 1) ∘ (i_{2}, k), Gauge(C, n + 1) ∘ (i_{1}, k)) meets LowerArc(C).

(26) Let C be a simple closed curve and i_{1}, i_{2}, j, k be natural numbers. Suppose that 1 < i_{1} and i_{1} < lenGauge(C, n + 1) and 1 < i_{2} and i_{2} < lenGauge(C, n+1) and 1 j and j k and k widthGauge(C, n+1) and Gauge(C, n+1)∘(i_{1}, k) ∈ LowerArc(L̃(Cage(C, n+1))) and Gauge(C, n+ 1) ∘ (i_{2}, j) ∈ UpperArc(L̃(Cage(C, n + 1))). Then L(Gauge(C, n + 1) ∘ (i_{2}, j), Gauge(C, n + 1) ∘ (i_{2}, k)) ∪ L(Gauge(C, n + 1) ∘ (i_{2}, k), Gauge(C, n + 1) ∘ (i_{1}, k)) meets UpperArc(C).

(27) For every simple closed curve C and for every point p of E_{T}^{2} such that W-bound(C) < p_{1} and p_{1} < E-bound(C) holds p ∉ NorthArc(C) or p ∉ SouthArc(C).

(28) For every simple closed curve C and for every point p of E_{T}^{2} such that p_{1} = \frac{W-bound (C)+E-bound (C)}{2} holds p ∉ NorthArc(C) or p ∉ SouthArc(C).

References

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

[2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.

[3] Grzegorz Bancerek. Countable sets and Hessenberg’s theorem. Formalized Mathematics, 2(1):65–69, 1991.

[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 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. Gauges. Formalized Mathematics, 8(1):25–27, 1999.

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

[9] Czesław Byliński and Mariusz Żynel. Cages - the external approximation of Jordan’s curve. Formalized Mathematics, 9(1):19–24, 2001.

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

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

[12] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Arcs, line segments and special polygonal arcs. Formalized Mathematics, 2(5):617–621, 1991.

430 robert milewski

[13] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Simple closed curves. Formalized Mathematics, 2(5):663–664, 1991.

[14] Adam Grabowski. On the Kuratowski limit operators. Formalized Mathematics, 11(4):399–409, 2003.

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

[16] Katarzyna Jankowska. Matrices. Abelian group of matrices. Formalized Mathematics, 2(4):475–480, 1991.

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

[18] Artur Korniłowicz. Properties of left and right components. Formalized Mathematics, 8(1):163–168, 1999.

[19] Artur Korniłowicz, Robert Milewski, Adam Naumowicz, and Andrzej Trybulec. Gauges and cages. Part I. Formalized Mathematics, 9(3):501–509, 2001.

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

[21] Robert Milewski. Upper and lower sequence of a cage. Formalized Mathematics, 9(4):787– 790, 2001.

[22] Yatsuka Nakamura and Czesław Byliński. Extremal properties of vertices on special polygons. Part I. Formalized Mathematics, 5(1):97–102, 1996.

[23] Yatsuka Nakamura and Andrzej Trybulec. Decomposing a Go-board into cells. Formalized Mathematics, 5(3):323–328, 1996.

[24] Yatsuka Nakamura and Andrzej Trybulec. A decomposition of a simple closed curves and the order of their points. Formalized Mathematics, 6(4):563–572, 1997.

[25] Andrzej Nędzusiak. σ-fields and probability. Formalized Mathematics, 1(2):401–407, 1990.

[26] Beata Padlewska. Connected spaces. Formalized Mathematics, 1(1):239–244, 1990.

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

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

[29] Andrzej Trybulec. On the decomposition of finite sequences. Formalized Mathematics, 5(3):317–322, 1996.

[30] Andrzej Trybulec and Yatsuka Nakamura. On the order on a special polygon. Formalized Mathematics, 6(4):541–548, 1997.

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

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

Received September 27, 2003

on the upper and lower approximations … 431

alalalalalal alalalalalalal

Index of MML Identifiers

ABCMIZ 0 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .355 BHSP 6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 225 BHSP 7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 271 BINARI 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .417 BORSUK 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .313 COMPLEX2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 275 CONVEX2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 267 CONVEX3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 331 CONVFUN1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 349 EUCLID 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .281 EUCLID 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .371 EUCLID 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .381 FSCIRC 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .231 GRAPHSP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 237 GROEB 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 293 GROEB 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 303 INTPRO 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .259 JGRAPH 6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .213 JORDAN19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 425 JORDAN A . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .411 KURATO 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .323 KURATO 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .399 LFUZZY 0 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .393 MATRIX 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .385 MEMBERED . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 341 NECKLA 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .289 ROBBINS2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 335 RSSPACE2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255 RSSPACE3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 377 RSSPACE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 249 SCMPDS 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .421

Contents Formaliz. Math. 11 (4)

On the Sets Inhabited by Numbers

By Andrzej Trybulec  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 341

Definition of Convex Function and Jensen’s Inequality

By Grigory E. Ivanov  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 349

On Semilattice Structure of Mizar Types

By Grzegorz Bancerek  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 355

Lines in n-Dimensional Euclidean Spaces

By Akihiro Kubo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 371

Banach Space of Absolute Summable Real Sequences

By Yasumasa Suzuki et al. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 377

Cross Products and Tripple Vector Products in 3-dimensional Euc-

lidean Space

By Kanchun et al. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 381

Calculation of Matrices of Field Elements. Part I

By Yatsuka Nakamura and Hiroshi Yamazaki  . . . . . . . . . . . . 385

Lattice of Fuzzy Sets

By Takashi Mitsuishi and Grzegorz Bancerek  . . . . . . . . . . . 393

On the Kuratowski Limit Operators

By Adam Grabowski . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 399

On the Segmentation of a Simple Closed Curve

By Andrzej Trybulec  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 411

On the Calculus of Binary Arithmetics

By Shunichi Kobayashi  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 417

SCMPDS Is Not Standard

By Artur Korniłowicz and Yasunari Shidama  . . . . . . . . . . . 421

Continued on inside back cover

On the Upper and Lower Approximations of the Curve

By Robert Milewski  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 425

Index of MML Identifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 432