FORMALIZED MATHEMATICS Volume 6, Number 3, 1997 Warsaw University - Białystok

Basic Properties of Objects and Morphisms

Beata Madras-Kobus Warsaw University Białystok

MML Identifier: ALTCAT 3.

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

Let C be a non empty category structure with units, let o_{1}, o_{2} be objects of C, let A be a morphism from o_{1} to o_{2}, and let B be a morphism from o_{2} to o_{1}. We say that A is left inverse of B if and only if:

(Def. 1) A · B = id_{(o_{2})} .

We introduce B is right inverse of A as a synonym of A is left inverse of B.

Let C be a non empty category structure with units, let o_{1}, o_{2} be objects of C, and let A be a morphism from o_{1} to o_{2}. We say that A is retraction if and only if:

(Def. 2) There exists a morphism from o_{2} to o_{1} which is right inverse of A.

Let C be a non empty category structure with units, let o_{1}, o_{2} be objects of C, and let A be a morphism from o_{1} to o_{2}. We say that A is coretraction if and only if:

(Def. 3) There exists a morphism from o_{2} to o_{1} which is left inverse of A. Next we state the proposition

(1) Let C be a non empty category structure with units and o be an object of C. Then id_{o} is retraction and id_{o} is coretraction.

Let C be a category and let o_{1}, o_{2} be objects of C. Let us assume that ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{1}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2}. Let us assume that A is retraction and coretraction. The functor A^{−1} yields a morphism from o_{2} to o_{1} and is defined by:

(Def. 4) A^{−1} is left inverse of A and A^{−1} is right inverse of A.

We now state three propositions:

(2) Let C be a category and o_{1}, o_{2} be objects of C. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{1}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2}. If A is retraction and coretraction, then A^{−1} · A = id_{(o_{1})} and A · A^{−1} = id_{(o_{2})} .

(3) Let C be a category and o_{1}, o_{2} be objects of C. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{1}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2}. If A is retraction and coretraction, then (A^{−1} )^{−1} = A.

(4) For every category C and for every object o of C holds (id_{o})^{−1} = id_{o} . Let C be a category, let o_{1}, o_{2} be objects of C, and let A be a morphism

from o_{1} to o_{2}. We say that A is iso if and only if: (Def. 5) A · A^{−1} = id_{(o_{2})} and A^{−1} · A = id_{(o_{1})} .

One can prove the following three propositions:

(5) Let C be a category, o_{1}, o_{2} be objects of C, and A be a morphism from o_{1} to o_{2}. If A is iso, then A is retraction and coretraction.

(6) Let C be a category and o_{1}, o_{2} be objects of C. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{1}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2}. Then A is iso if and only if A is retraction and coretraction.

(7) Let C be a category, o_{1}, o_{2}, o_{3} be objects of C, A be a morphism from o_{1} to o_{2}, and B be a morphism from o_{2} to o_{3}. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{3}⟩ ≠ ∅ and ⟨o_{3}, o_{1}⟩ ≠ ∅ and A is iso and B is iso. Then B · A is iso and (B · A)^{−1} = A^{−1} · B^{−1} .

Let C be a category and let o_{1}, o_{2} be objects of C. We say that o_{1}, o_{2} are iso if and only if:

(Def. 6) ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{1}⟩ ≠ ∅ and there exists a morphism from o_{1} to o_{2}

which is iso. Let us note that the predicate o_{1}, o_{2} are iso is reflexive and symmetric.

One can prove the following proposition

(8) Let C be a category and o_{1}, o_{2}, o_{3} be objects of C. If o_{1}, o_{2} are iso and o_{2}, o_{3} are iso , then o_{1}, o_{3} are iso .

Let C be a non empty category structure, let o_{1}, o_{2} be objects of C, and let A be a morphism from o_{1} to o_{2}. We say that A is mono if and only if:

(Def. 7) For every object o of C such that ⟨o, o_{1}⟩ ≠ ∅ and for all morphisms B,

C from o to o_{1} such that A · B = A · C holds B = C. Let C be a non empty category structure, let o_{1}, o_{2} be objects of C, and let

A be a morphism from o_{1} to o_{2}. We say that A is epi if and only if: (Def. 8) For every object o of C such that ⟨o_{2}, o⟩ ≠ ∅ and for all morphisms B,

C from o_{2} to o such that B · A = C · A holds B = C. We now state a number of propositions:

(9) Let C be an associative transitive non empty category structure and o_{1}, o_{2}, o_{3} be objects of C. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{3}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2} and B be a morphism from o_{2} to o_{3}. If A is mono and B is mono, then B · A is mono.

(10) Let C be an associative transitive non empty category structure and o_{1}, o_{2}, o_{3} be objects of C. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{3}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2} and B be a morphism from o_{2} to o_{3}. If A is epi and B is epi, then B · A is epi.

(11) Let C be an associative transitive non empty category structure and o_{1}, o_{2}, o_{3} be objects of C. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{3}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2} and B be a morphism from o_{2} to o_{3}. If B · A is mono, then A is mono.

(12) Let C be an associative transitive non empty category structure and o_{1}, o_{2}, o_{3} be objects of C. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{3}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2} and B be a morphism from o_{2} to o_{3}. If B · A is epi, then B is epi.

(13) Let X be a non empty set and o_{1}, o_{2} be objects of Ens_{X}. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2} and F be a function from o_{1} into o_{2}. If F = A, then A is mono iff F is one-to-one.

(14) Let X be a non empty set with non empty elements and o_{1}, o_{2} be objects of Ens_{X}. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2} and F be a function from o_{1} into o_{2}. If F = A, then A is epi iff F is onto.

(15) Let C be a category and o_{1}, o_{2} be objects of C. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{1}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2}. If A is retraction, then A is epi.

(16) Let C be a category and o_{1}, o_{2} be objects of C. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{1}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2}. If A is coretraction, then A is mono.

(17) Let C be a category and o_{1}, o_{2} be objects of C. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{1}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2}. If A is iso, then A is mono and epi.

(18) Let C be a category and o_{1}, o_{2}, o_{3} be objects of C. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{3}⟩ ≠ ∅ and ⟨o_{3}, o_{1}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2} and B be a morphism from o_{2} to o_{3}. If A is retraction and B is retraction, then B · A is retraction.

(19) Let C be a category and o_{1}, o_{2}, o_{3} be objects of C. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{3}⟩ ≠ ∅ and ⟨o_{3}, o_{1}⟩ ≠ ∅. Let A be a morphism from o_{1} to o_{2} and B be a morphism from o_{2} to o_{3}. If A is coretraction and B is coretraction, then B · A is coretraction.

(20) Let C be a category, o_{1}, o_{2} be objects of C, and A be a morphism from o_{1} to o_{2}. If A is retraction and mono and ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{1}⟩ ≠ ∅, then A is iso.

(21) Let C be a category, o_{1}, o_{2} be objects of C, and A be a morphism from o_{1} to o_{2}. If A is coretraction and epi and ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{1}⟩ ≠ ∅, then A is iso.

(22) Let C be a category, o_{1}, o_{2}, o_{3} be objects of C, A be a morphism from o_{1} to o_{2}, and B be a morphism from o_{2} to o_{3}. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{3}⟩ ≠ ∅ and ⟨o_{3}, o_{1}⟩ ≠ ∅ and B · A is retraction. Then B is retraction.

(23) Let C be a category, o_{1}, o_{2}, o_{3} be objects of C, A be a morphism from o_{1} to o_{2}, and B be a morphism from o_{2} to o_{3}. Suppose ⟨o_{1}, o_{2}⟩ ≠ ∅ and ⟨o_{2}, o_{3}⟩ ≠ ∅ and ⟨o_{3}, o_{1}⟩ ≠ ∅ and B · A is coretraction. Then A is coretraction.

(24) Let C be a category. Suppose that for all objects o_{1}, o_{2} of C holds every morphism from o_{1} to o_{2} is retraction. Let a, b be objects of C and A be a morphism from a to b. If ⟨a, b⟩ ≠ ∅ and ⟨b, a⟩ ≠ ∅, then A is iso.

Let C be a non empty category structure with units and let o be an object of C. Note that there exists a morphism from o to o which is mono, epi, retraction, and coretraction.

Let C be a category and let o be an object of C. Observe that there exists a morphism from o to o which is mono, epi, iso, retraction, and coretraction.

Let C be a category, let o be an object of C, and let A, B be mono morphisms from o to o. Note that A · B is mono.

Let C be a category, let o be an object of C, and let A, B be epi morphisms from o to o. Observe that A · B is epi.

Let C be a category, let o be an object of C, and let A, B be iso morphisms from o to o. One can verify that A · B is iso.

Let C be a category, let o be an object of C, and let A, B be retraction morphisms from o to o. Observe that A · B is retraction.

Let C be a category, let o be an object of C, and let A, B be coretraction morphisms from o to o. One can check that A · B is coretraction.

Let C be a graph and let o be an object of C. We say that o is initial if and only if:

(Def. 9) For every object o_{1} of C there exists a morphism M from o to o_{1} such

that M ∈ ⟨o, o_{1}⟩ and ⟨o, o_{1}⟩ is trivial. One can prove the following two propositions:

(25) Let C be a graph and o be an object of C. Then o is initial if and only if for every object o_{1} of C there exists a morphism M from o to o_{1} such that M ∈ ⟨o, o_{1}⟩ and for every morphism M_{1} from o to o_{1} such that M_{1} ∈ ⟨o, o_{1}⟩ holds M = M_{1}.

(26) For every category C and for all objects o_{1}, o_{2} of C such that o_{1} is initial

and o_{2} is initial holds o_{1}, o_{2} are iso . Let C be a graph and let o be an object of C. We say that o is terminal if

and only if: (Def. 10) For every object o_{1} of C there exists a morphism M from o_{1} to o such

that M ∈ ⟨o_{1}, o⟩ and ⟨o_{1}, o⟩ is trivial. Next we state two propositions:

(27) Let C be a graph and o be an object of C. Then o is terminal if and only if for every object o_{1} of C there exists a morphism M from o_{1} to o such that M ∈ ⟨o_{1}, o⟩ and for every morphism M_{1} from o_{1} to o such that M_{1} ∈ ⟨o_{1}, o⟩ holds M = M_{1}.

(28) For every category C and for all objects o_{1}, o_{2} of C such that o_{1} is

terminal and o_{2} is terminal holds o_{1}, o_{2} are iso . Let C be a graph and let o be an object of C. We say that o is zero if and

only if: (Def. 11) o is initial and terminal.

We now state the proposition

(29) For every category C and for all objects o_{1}, o_{2} of C such that o_{1} is zero

and o_{2} is zero holds o_{1}, o_{2} are iso . Let C be a non empty category structure, let o_{1}, o_{2} be objects of C, and

let M be a morphism from o_{1} to o_{2}. We say that M is zero if and only if the condition (Def. 12) is satisfied.

(Def. 12) Let o be an object of C. Suppose o is zero. Let A be a morphism from

o_{1} to o and B be a morphism from o to o_{2}. Then M = B · A. We now state the proposition

(30) Let C be a category, o_{1}, o_{2}, o_{3} be objects of C, M_{1} be a morphism from o_{1} to o_{2}, and M_{2} be a morphism from o_{2} to o_{3}. If M_{1} is zero and M_{2} is zero, then M_{2} · M_{1} is zero.

References

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

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

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

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

[5] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Formalized Mathematics, 3(2):151–160, 1992.

[6] Yozo Toda. The formalization of simple graphs. Formalized Mathematics, 5(1):137–144, 1996.

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

[8] Andrzej Trybulec. Categories without uniqueness of cod and dom. Formalized Mathematics, 5(2):259–267, 1996.

334 beata madras-kobus

[9] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

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

Abian’s Fixed Point Theorem^{1}

Piotr Rudnicki University of Alberta Edmonton Andrzej Trybulec Warsaw University Białystok

Summary. A. Abian [1] proved the following theorem:

Let f be a mapping from a finite set D. Then f has a fixed point if and only if D is not a union of three mutually disjoint sets A, B and C such that

A ∩ f[A] = B ∩ f[B] = C ∩ f[C] = ∅.

(The range of f is not necessarily the subset of its domain). The proof of the sufficiency is by induction on the number of elements of D. A.Ma̧kowski and K.Wiśniewski [12] have shown that the assumption of finiteness is superfluous. They proved their version of the theorem for f being a function from D into D. In the proof, the required partition was constructed and the construction used the axiom of choice. Their main point was to demonstrate that the use of this axiom in the proof is essential. We have proved in Mizar the generalized version of Abian’s theorem, i.e. without assuming finiteness of D. We have simplified the proof from [12] which uses well-ordering principle and transfinite ordinals—our proof does not use these notions but otherwise is based on their idea (we employ choice functions).

MML Identifier: ABIAN.

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

1This work was partially supported by NSERC Grant OGP9207 and NATO CRG 951368.

1. Preliminaries

For simplicity, we adopt the following rules: x, y, E, E_{1}, E_{2}, E_{3} are sets, s_{1} is a family of subsets of E, f is a function from E into E, and k, l, n are natural numbers.

Let i be an integer. We say that i is even if and only if: (Def. 1) There exists an integer j such that i = 2 · j.

We introduce i is odd as an antonym of i is even.

Let n be a natural number. Let us observe that n is even if and only if: (Def. 2) There exists k such that n = 2 · k.

We introduce n is odd as an antonym of n is even.

One can check the following observations:

∗ there exists a natural number which is even,

∗ there exists a natural number which is odd,

∗ there exists an integer which is even, and

∗ there exists an integer which is odd. One can prove the following proposition

(1) For every integer i holds i is odd iff there exists an integer j such that i = 2 · j + 1.

Let i be an integer. Note that 2 · i is even. Let i be an even integer. Note that i + 1 is odd. Let i be an odd integer. Observe that i + 1 is even. Let i be an even integer. One can verify that i − 1 is odd. Let i be an odd integer. Note that i − 1 is even. Let i be an even integer and let j be an integer. One can check that i · j is

even and j · i is even.

Let i, j be odd integers. Note that i · j is odd. Let i, j be even integers. One can check that i + j is even. Let i be an even integer and let j be an odd integer. Note that i + j is odd

and j + i is odd.

Let i, j be odd integers. Observe that i + j is even. Let i be an even integer and let j be an odd integer. Observe that i − j is

odd and j − i is odd.

Let i, j be odd integers. One can verify that i − j is even. Let us consider E, f, n. Then f^{n} is a function from E into E. Let A be a set and let B be a set with a non-empty element. One can verify

that there exists a function from A into B which is non-empty.

Let A be a non empty set, let B be a set with a non-empty element, let f be a non-empty function from A into B, and let a be an element of A. One can verify that f(a) is non empty.

Let X be a non empty set. Note that 2^{X} has a non-empty element. We now state two propositions:

(2) For every non empty subset S of ℕ such that 0 ∈ S holds minS = 0.

(3) For every non empty set E and for every function f from E into E and for every element x of E holds f^{0}(x) = x.

Let f be a function. We say that f has a fixpoint if and only if: (Def. 3) There exists x which is a fixpoint of f.

We introduce f has no fixpoint as an antonym of f has a fixpoint.

Let X be a set and let x be an element of X. We say that x is covering if and only if:

(Def. 4) ⋃ x = ⋃ ⋃ X.

One can prove the following proposition

(4) s_{1} is covering iff ⋃ s_{1} = E. Let us consider E. One can verify that there exists a family of subsets of E

which is non empty, finite, and covering.

2. Abian’s Theorem

One can prove the following proposition

(5) Let E be a set, f be a function from E into E, and s_{1} be a non empty covering family of subsets of E such that for every element X of s_{1} holds X misses f^{∘}X. Then f has no fixpoint.

Let us consider E, f. The functor f_{≡} yielding an equivalence relation of E is defined by:

(Def. 5) For all x, y such that x ∈ E and y ∈ E holds ⟨⟨x, y⟩⟩∈ f_{≡} iff there exist

k, l such that f^{k}(x) = f^{l}(y). One can prove the following three propositions:

(6) Let E be a non empty set, f be a function from E into E, c be an element of Classes(f_{≡} ), and e be an element of c. Then f(e) ∈ c.

(7) Let E be a non empty set, f be a function from E into E, c be an element of Classes(f_{≡} ), e be an element of c, and given n. Then f^{n}(e) ∈ c.

(8) Let E be a non empty set and f be a function from E into E. Suppose f has no fixpoint. Then there exist E_{1}, E_{2}, E_{3} such that E_{1} ∪ E_{2} ∪ E_{3} = E and f^{∘}E_{1} misses E_{1} and f^{∘}E_{2} misses E_{2} and f^{∘}E_{3} misses E_{3}.

338 piotr rudnicki and andrzej trybulec

References

[1] A. Abian. A fixed point theorem. Nieuw Arch. Wisk., 3(16):184–185, 1968.

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

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

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

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

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

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

[8] Agata Darmochwał and Andrzej Trybulec. Similarity of formulae. Formalized Mathematics, 2(5):635–642, 1991.

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

[10] Jarosław Kotowicz, Beata Madras, and Małgorzata Korolkiewicz. Basic notation of universal algebra. Formalized Mathematics, 3(2):251–253, 1992.

[11] Beata Madras. On the concept of the triangulation. Formalized Mathematics, 5(3):457– 462, 1996.

[12] A. Mąkowski and K. Wiśniewski. Generalization of Abian’s fixed point theorem. Annales Soc. Math. Pol. Series I, XIII:63–65, 1969.

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

[14] Konrad Raczkowski and Paweł Sadowski. Equivalence relations and classes of abstraction. Formalized Mathematics, 1(3):441–444, 1990.

[15] Piotr Rudnicki and Andrzej Trybulec. Fixpoints in complete lattices. Formalized Mathematics, 6(1):109–115, 1997.

[16] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329–334, 1990.

[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. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

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

[21] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

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

On Same Equivalents of Well-foundedness^{1}

Piotr Rudnicki University of Alberta Edmonton Andrzej Trybulec Warsaw University Białystok

Summary. Four statements equivalent to well-foundedness (well-founded induction, existence of recursively defined functions, uniqueness of recursively defined functions, and absence of descending ω-chains) have been proved in Mizar and the proofs were mechanically checked for correctness. It seems not to be widely known that the existence (without the uniqueness assumption) of recursively defined functions implies well-foundedness. In the proof we used regular cardinals, a fairly advanced notion of set theory. This work was inspired by T. Franzen’s paper [17]. Franzen’s proofs were written by a mathematician having an argument with a computer scientist. We were curious about the effort needed to formalize Franzen’s proofs given the state of the Mizar Mathematical Library at that time (July 1996). The formalization went quite smoothly once the mathematics was sorted out.

MML Identifier: WELLFND1.

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

1. Preliminaries

Let R be a 1-sorted structure, let X be a set, and let p be a partial function from the carrier of R to X. Then domp is a subset of R.

Next we state two propositions:

(1) For every set X and for all functions f, g such that f ⊆ g and X ⊆ domf holds f↾X = g↾X.

1This work was partially supported by NSERC Grant OGP9207 and NATO CRG 951368.

(2) Let X be a functional set. Suppose that for all functions f, g such that f ∈ X and g ∈ X holds f ≈ g. Then ⋃ X is a function.

The scheme PFSeparation concerns sets A, B and a unary predicate P, and states that:

There exists a subset P_{1} of A ˙→ B such that for every partial function p_{1} from A to B holds p_{1} ∈ P_{1} iff P[p_{1}]

for all values of the parameters.

Let X be a set. Observe that X^{+} is non empty. Let us note that there exists an aleph which is regular. One can prove the following two propositions:

(3) For every regular aleph M and for every set X such that X ⊆ M and \overline{\overline{X}} ∈ M holds supX ∈ M.

(4) For every relational structure R and for every set x holds (the internal relation of R)-Seg(x) ⊆ the carrier of R.

Let R be a relational structure and let X be a subset of R. Let us observe that X is lower if and only if:

(Def. 1) For all sets x, y such that x ∈ X and ⟨⟨y, x⟩⟩∈ the internal relation of R

holds y ∈ X. Next we state two propositions:

(5) Let R be a relational structure, X be a subset of R, and x be a set. If X is lower and x ∈ X, then (the internal relation of R)-Seg(x) ⊆ X.

(6) Let R be a relational structure, X be a lower subset of R, Y be a subset of R, and x be a set. If Y = X ∪{x} and (the internal relation of R)-Seg(x) ⊆ X, then Y is lower.

2. Well Founded Relational Structures

Let R be a relational structure. We say that R is well founded if and only if: (Def. 2) The internal relation of R is well founded in the carrier of R.

Let us mention that there exists a relational structure which is non empty and well founded.

Let R be a relational structure and let X be a subset of R. We say that X is well founded if and only if:

(Def. 3) The internal relation of R is well founded in X.

Let R be a relational structure. Note that there exists a subset of R which is well founded.

Let R be a relational structure. The functor WF-Part(R) yielding a subset of R is defined by:

(Def. 4) WF-Part(R) = ⋃{S, S ranges over subsets of R: S is well founded and

lower}. Let R be a relational structure. One can verify that WF-Part(R) is lower

and well founded.

One can prove the following four propositions:

(7) Let R be a non empty relational structure and x be an element of the carrier of R. Then {x} is a well founded subset of R.

(8) Let R be a relational structure and X, Y be well founded subsets of R. If X is lower, then X ∪ Y is a well founded subset of R.

(9) For every relational structure R holds R is well founded iff WF-Part(R) = the carrier of R.

(10) Let R be a non empty relational structure and x be an element of the carrier of R. If (the internal relation of R)-Seg(x) ⊆ WF-Part(R), then x ∈ WF-Part(R).

The scheme WFMin deals with a non empty relational structure A, an element B of A, and a unary predicate P, and states that:

There exists an element x of A such that P[x] and it is not true that there exists an element y of A such that x ≠ y and P[y] and ⟨⟨y, x⟩⟩∈ the internal relation of A

provided the parameters meet the following requirements:

• P[B], and

• A is well founded. We now state the proposition

(11) Let R be a non empty relational structure. Then R is well founded if and only if for every set S such that for every element x of the carrier of R such that (the internal relation of R)-Seg(x) ⊆ S holds x ∈ S holds the carrier of R ⊆ S.

The scheme WFInduction deals with a non empty relational structure A and a unary predicate P, and states that:

For every element x of A holds P[x] provided the parameters meet the following conditions:

• Let x be an element of A. Suppose that for every element y of A such that y ≠ x and ⟨⟨y, x⟩⟩ ∈ the internal relation of A holds P[y]. Then P[x], and

• A is well founded. Let R be a non empty relational structure, let V be a non empty set, let H

be a function from [: the carrier of R, (the carrier of R) ˙→ V :] into V, and let F be a function. We say that F is recursively expressed by H if and only if:

(Def. 5) For every element x of the carrier of R holds F (x) = H(⟨⟨x, F ↾(the internal relation of R)-Seg(x)⟩⟩).

One can prove the following propositions:

(12) Let R be a non empty relational structure. Then R is well founded if and only if for every non empty set V and for every function H from [: the carrier of R, (the carrier of R) ˙→ V :] into V holds there exists a function from the carrier of R into V which is recursively expressed by H.

(13) Let R be a non empty relational structure and V be a non trivial set. Suppose that for every function H from [: the carrier of R, (the carrier of R) ˙→ V :] into V and for all functions F_{1}, F_{2} from the carrier of R into V such that F_{1} is recursively expressed by H and F_{2} is recursively expressed by H holds F_{1} = F_{2}. Then R is well founded.

(14) Let R be a non empty well founded relational structure, V be a non empty set, H be a function from [: the carrier of R, (the carrier of R) ˙→ V :] into V, and F_{1}, F_{2} be functions from the carrier of R into V. Suppose F_{1} is recursively expressed by H and F_{2} is recursively expressed by H. Then F_{1} = F_{2}.

Let S be a set. Let us assume that contradiction.^{2} (Def. 6) choose(S) is an element of S.

Let R be a relational structure and let f be a sequence of R. We say that f is descending if and only if:

(Def. 7) For every natural number n holds f(n+1) ≠ f(n) and ⟨⟨f(n+1), f(n)⟩⟩∈

the internal relation of R. One can prove the following proposition

(15) For every non empty relational structure R holds R is well founded iff there exists no sequence of R which is descending.

References

[1] Grzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543–547, 1990.

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

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

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

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

[6] Grzegorz Bancerek. The well ordering relations. Formalized Mathematics, 1(1):123–129, 1990.

[7] Grzegorz Bancerek. On powers of cardinals. Formalized Mathematics, 3(1):89–93, 1992.

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

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

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

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

2This definition is absolutely permissive, i.e. we assume a contradiction, but we are interested only in the type of the functor ‘choose’.

on same equivalents of well-foundedness 343

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

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

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

[15] Patricia L. Carlson and Grzegorz Bancerek. Context-free grammar - part 1. Formalized Mathematics, 2(5):683–687, 1991.

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

[17] T. Franzen. Teaching mathematics through formalism: a few caveats. In D. Gries, editor, Proceedings of the DIMACS Symposium on Teaching Logic. DIMACS, 1996. On WWW: http://dimacs.rutgers.edu/Workshops/Logic/program.html.

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

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

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

[21] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329–334, 1990.

[22] Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1(3):495–500, 1990.

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

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

[25] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

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

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

344 piotr rudnicki and andrzej trybulec

Algebraic and Arithmetic Lattices. Part I^{1}

Robert Milewski Warsaw University Białystok

Summary. We formalize [10, pp.87–89]

MML Identifier: WAYBEL13.

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

1. Preliminaries

The scheme LambdaCD deals with a non empty set A, a unary functor F yielding a set, a unary functor G yielding a set, and a unary predicate P, and states that:

There exists a function f such that domf = A and for every element x of A holds if P[x], then f(x) = F(x) and if not P[x], then f(x) = G(x)

for all values of the parameters.

The following propositions are true:

(1) Let L be a non empty reflexive transitive relational structure and x, y be elements of L. If x y, then compactbelow(x) ⊆ compactbelow(y).

(2) For every non empty reflexive relational structure L and for every element x of L holds compactbelow(x) is a subset of CompactSublatt(L).

(3) For every relational structure L and for every relational substructure S of L holds every subset of S is a subset of L.

1This work was partially supported by KBN Grant 8 T11C 018 12.

(4) For every non empty reflexive transitive relational structure L with l.u.b.’s holds the carrier of L is an ideal of L.

(5) Let L_{1} be a lower-bounded non empty reflexive antisymmetric relational structure and L_{2} be a non empty reflexive antisymmetric relational structure. Suppose the relational structure of L_{1} = the relational structure of L_{2} and L_{1} is up-complete. Then the carrier of CompactSublatt(L_{1}) = the carrier of CompactSublatt(L_{2}).

2. Algebraic and Arithmetic Lattices

Next we state three propositions:

(6) For every algebraic lower-bounded lattice L holds every continuous subframe of L is algebraic.

(7) Let X, E be sets and L be a continuous subframe of 2_{⊆}^{X}. Then E ∈ the carrier of CompactSublatt(L) if and only if there exists an element F of 2_{⊆}^{X} such that F is finite and E = ⋂{Y, Y ranges over elements of L: F ⊆ Y } and F ⊆ E.

(8) For every lower-bounded sup-semilattice L holds ⟨Ids(L), ⊆⟩ is a continuous subframe of 2_{⊆}^{the carrier of L}.

Let L be a non empty reflexive transitive relational structure. Observe that there exists an ideal of L which is principal.

One can prove the following propositions:

(9) For every lower-bounded sup-semilattice L and for every non empty directed subset X of ⟨Ids(L), ⊆⟩ holds supX = ⋃ X.

(10) For every lower-bounded sup-semilattice S holds ⟨Ids(S), ⊆⟩ is algebraic.

(11) Let S be a lower-bounded sup-semilattice and x be an element of ⟨Ids(S), ⊆⟩. Then x is compact if and only if x is a principal ideal of S.

(12) Let S be a lower-bounded sup-semilattice and x be an element of ⟨Ids(S), ⊆⟩. Then x is compact if and only if there exists an element a of S such that x = ↓a.

(13) Let L be a lower-bounded sup-semilattice and f be a map from L into CompactSublatt(⟨Ids(L), ⊆⟩). If for every element x of L holds f(x) = ↓x, then f is isomorphic.

(14) For every lower-bounded lattice S holds ⟨Ids(S), ⊆⟩ is arithmetic.

(15) For every lower-bounded sup-semilattice L holds CompactSublatt(L) is a lower-bounded sup-semilattice.

(16) Let L be an algebraic lower-bounded sup-semilattice and f be a map from L into ⟨Ids(CompactSublatt(L)), ⊆⟩. If for every element x of L holds f(x) = compactbelow(x), then f is isomorphic.

(17) Let L be an algebraic lower-bounded sup-semilattice and x be an element of L. Then compactbelow(x) is a principal ideal of CompactSublatt(L) if and only if x is compact.

3. Maps

We now state three propositions:

(18) Let L_{1}, L_{2} be non empty relational structures, X be a subset of L_{1}, x be an element of L_{1}, and f be a map from L_{1} into L_{2}. If f is isomorphic, then x X iff f(x) f^{∘}X.

(19) Let L_{1}, L_{2} be non empty relational structures, X be a subset of L_{1}, x be an element of L_{1}, and f be a map from L_{1} into L_{2}. If f is isomorphic, then x X iff f(x) f^{∘}X.

(20) Let L_{1}, L_{2} be non empty antisymmetric relational structures and f be a map from L_{1} into L_{2}. If f is isomorphic, then f is infs-preserving and sups-preserving.

Let L_{1}, L_{2} be non empty antisymmetric relational structures. Note that every map from L_{1} into L_{2} which is isomorphic is also infs-preserving and supspreserving.

We now state a number of propositions:

(21) Let L_{1}, L_{2}, L_{3} be non empty transitive antisymmetric relational structures and f be a map from L_{1} into L_{2}. Suppose f is infs-preserving. Suppose L_{2} is a full infs-inheriting relational substructure of L_{3} and L_{3} is complete. Then there exists a map g from L_{1} into L_{3} such that f = g and g is infspreserving.

(22) Let L_{1}, L_{2}, L_{3} be non empty transitive antisymmetric relational structures and f be a map from L_{1} into L_{2}. Suppose f is monotone and directedsups-preserving. Suppose L_{2} is a full directed-sups-inheriting relational substructure of L_{3} and L_{3} is complete. Then there exists a map g from L_{1} into L_{3} such that f = g and g is directed-sups-preserving.

(23) For every lower-bounded sup-semilattice L holds ⟨Ids(CompactSublatt (L)), ⊆⟩ is a continuous subframe of 2_{⊆}^{the carrier of CompactSublatt (L)}.

(24) Let L be an algebraic lower-bounded lattice. Then there exists a map g

from L into 2_{⊆}^{the carrier of CompactSublatt (L)} such that

(i) g is infs-preserving, directed-sups-preserving, and one-to-one, and (ii) for every element x of L holds g(x) = compactbelow(x).

(25) 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 an algebraic lower-bounded lattice. Then ∏ J is an algebraic lower-bounded lattice.

(26) Let L_{1}, L_{2} be non empty relational structures. Suppose the relational structure of L_{1} = the relational structure of L_{2}. Then L_{1} and L_{2} are isomorphic.

(27) Let L_{1}, L_{2} be up-complete non empty posets and f be a map from L_{1} into L_{2}. Suppose f is isomorphic. Let x, y be elements of L_{1}. Then x ≪ y if and only if f(x) ≪ f(y).

(28) Let L_{1}, L_{2} be up-complete non empty posets and f be a map from L_{1} into L_{2}. Suppose f is isomorphic. Let x be an element of L_{1}. Then x is compact if and only if f(x) is compact.

(29) Let L_{1}, L_{2} be up-complete non empty posets and f be a map from L_{1} into L_{2}. If f is isomorphic, then for every element x of L_{1} holds f^{∘} compactbelow(x) = compactbelow(f(x)).

(30) For all non empty posets L_{1}, L_{2} such that L_{1} and L_{2} are isomorphic and L_{1} is up-complete holds L_{2} is up-complete.

(31) For all non empty posets L_{1}, L_{2} such that L_{1} and L_{2} are isomorphic and L_{1} is complete and satisfies axiom K holds L_{2} satisfies axiom K.

(32) Let L_{1}, L_{2} be sup-semilattices. Suppose L_{1} and L_{2} are isomorphic and L_{1} is lower-bounded and algebraic. Then L_{2} is algebraic.

(33) For every continuous lower-bounded sup-semilattice L holds SupMap(L) is infs-preserving and sups-preserving.

(34) Let L be a lower-bounded lattice. Then L is algebraic if and only if there exists a set X and there exists a full relational substructure S of 2_{⊆}^{X} such that S is infs-inheriting and directed-sups-inheriting and L and S are isomorphic.

(35) Let L be a lower-bounded lattice. Then L is algebraic if and only if there exists a set X and there exists a closure map c from 2_{⊆}^{X} into 2_{⊆}^{X} such that c is directed-sups-preserving and L and Imc are isomorphic.

References

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

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

[3] Grzegorz Bancerek. Closure operators and subalgebras. Formalized Mathematics, 6(2):295–301, 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,

algebraic and arithmetic lattices. part i 349

[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. Galois connections. Formalized Mathematics, 6(1):131–143, 1997.

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

[10] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, Berlin, Heidelberg, New York, 1980.

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

[12] Robert Milewski. Algebraic lattices. Formalized Mathematics, 6(2):249–254, 1997.

[13] Michał Muzalewski. Categories of groups. Formalized Mathematics, 2(4):563–571, 1991.

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

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

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

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

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

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

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

[21] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

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

[23] Mariusz Żynel. The equational characterization of continuous lattices. Formalized Mathematics, 6(2):199–205, 1997.

[24] Mariusz Żynel and Czesław Byliński. Properties of relational structures, posets, lattices and maps. Formalized Mathematics, 6(1):123–130, 1997.

Received March 4, 1997 350 robert milewski

Subsequences of Standard Special Circular Sequences in E_{T}^{2}

Yatsuka Nakamura Shinshu University

Nagano Roman Matuszewski^{1} Warsaw University Białystok Adam Grabowski^{2} Warsaw University Białystok

Summary. It is known that a standard special circular sequence in E_{T}^{2} properly defines a special polygon. We are interested in a part of such a sequence. It is shown that if the first point and the last point of the subsequence are different, it becomes a special polygonal sequence. The concept of �a part of” is introduced, and the subsequence having this property can be characterized by using �mid” function. For such subsequences, the concepts of �Upper” and �Lower” parts are introduced.

MML Identifier: JORDAN4.

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

1. Preliminaries

We adopt the following convention: i, i_{1}, i_{2}, i_{3}, j, k, n denote natural numbers and r_{1}, r_{2}, s, s_{1} denote real numbers.

The following propositions are true:

(1) If n − ′i = 0, then n i.

(2) If i j, then (j + k) − ′i = (j + k) − i.

1This paper was written while the author visited Shinshu University in fall 1996. 2This paper was written while the author visited Shinshu University in winter 1997.

(3) If i j, then (j + k) − ′i = j − ′i + k.

(4) If i_{1} ≠ 0 and i_{2} = i_{3} · i_{1}, then i_{3} i_{2}.

(5) If i_{1} < i_{2}, then i_{1} ÷ i_{2} = 0.

(6) If 0 < j and j < i and i < j + j, then i mod j ≠ 0.

(7) If 0 < j and j i and i < j + j, then i modj = i − j and i modj = i − ′j.

(8) If 0 < j, then (j + j) mod j = 0 and k · j mod j = 0.

(9) If 0 < k and k j and k mod j = 0, then k = j.

(10) (r_{1} + s_{1} + r_{2}) − s_{1} = r_{1} + r_{2} and (r_{1} − s_{1}) + r_{2} + s_{1} = r_{1} + r_{2} and (r_{1} + s_{1}) − r_{2} − s_{1} = r_{1} − r_{2} and (r_{1} − s_{1} − r_{2}) + s_{1} = r_{1} − r_{2}.

(11) r_{1} − r_{1} − r_{2} = − r_{2} and (− r_{1} + r_{1}) − r_{2} = − r_{2} and r_{1} − r_{2} − r_{1} = − r_{2} and (− r_{1} − r_{2}) + r_{1} = − r_{2}.

(12) If 0 < s and if s · r_{1} s · r_{2} or r_{1} · s r_{2} · s, then r_{1} r_{2}.

(13) If 0 < s and if s · r_{1} < s · r_{2} or r_{1} · s < r_{2} · s, then r_{1} < r_{2}.

2. Some facts about cutting of finite sequences

In the sequel D denotes a non empty set, f_{1} denotes a finite sequence of elements of D, and f denotes a non constant standard special circular sequence.

We now state a number of propositions:

(14) For every f_{1} such that f_{1} is circular and 1 lenf_{1} holds f_{1}(1) = f_{1}(lenf_{1}).

(15) For all f_{1}, i_{1}, i_{2} such that i_{1} i_{2} holds f_{1}↾i_{1}↾i_{2} = f_{1}↾i_{1} and f_{1}↾i_{2}↾i_{1} = f_{1}↾i_{1}.

(16) ε_{D}↾i = ε_{D}.

(17) Rev(ε_{D}) = ε_{D}.

(18) For all f_{1}, k such that k < lenf_{1} holds (f_{1})_{⇂k}(len((f_{1})_{⇂k})) = f_{1}(lenf_{1}) and π_{len((f_{1})_{⇂k})}(f_{1})_{⇂k} = π_{len f_{1}}f_{1}.

(19) Let g be a finite sequence of elements of E_{T}^{2} and given i. If g is a special sequence and i + 1 < leng, then g_{⇂i} is a special sequence.

(20) For all f_{1}, i_{1}, i_{2} such that 1 i_{2} and i_{2} i_{1} and i_{1} lenf_{1} holds lenmid(f_{1}, i_{2}, i_{1}) = i_{1} − ′i_{2} + 1.

(21) For all f_{1}, i_{1}, i_{2} such that 1 i_{2} and i_{2} i_{1} and i_{1} lenf_{1} holds lenmid(f_{1}, i_{1}, i_{2}) = i_{1} − ′i_{2} + 1.

(22) For all f_{1}, i_{1}, i_{2}, j such that 1 i_{1} and i_{1} i_{2} and i_{2} lenf_{1} holds (mid(f_{1}, i_{1}, i_{2}))(lenmid(f_{1}, i_{1}, i_{2})) = f_{1}(i_{2}).

(23) For all f_{1}, i_{1}, i_{2}, j such that 1 i_{1} and i_{1} lenf_{1} and 1 i_{2} and i_{2} lenf_{1} holds (mid(f_{1}, i_{1}, i_{2}))(lenmid(f_{1}, i_{1}, i_{2})) = f_{1}(i_{2}).

(24) For all f_{1}, i_{1}, i_{2}, j such that 1 i_{2} and i_{2} i_{1} and i_{1} lenf_{1} and 1 j and j i_{1} − ′i_{2} + 1 holds (mid(f_{1}, i_{1}, i_{2}))(j) = f_{1}(i_{1} − ′j + 1).

(25) Let given f_{1}, i_{1}, i_{2}. Suppose 1 i_{2} and i_{2} i_{1} and i_{1} lenf_{1} and 1 j and j i_{1} − ′i_{2} + 1. Then (mid(f_{1}, i_{1}, i_{2}))(j) = (mid(f_{1}, i_{2}, i_{1}))((((i_{1} − i_{2}) + 1) − j) + 1) and (((i_{1} − i_{2}) + 1) − j) + 1 = (i_{1} − ′i_{2} + 1) − ′j + 1.

(26) Let given f_{1}, i_{1}, i_{2}. Suppose 1 i_{1} and i_{1} i_{2} and i_{2} lenf_{1} and 1 j and j i_{2} − ′i_{1} + 1. Then (mid(f_{1}, i_{1}, i_{2}))(j) = (mid(f_{1}, i_{2}, i_{1}))((((i_{2} − i_{1}) + 1) − j) + 1) and (((i_{2} − i_{1}) + 1) − j) + 1 = (i_{2} − ′i_{1} + 1) − ′j + 1.

(27) For all f_{1}, k such that 1 k and k lenf_{1} holds mid(f_{1}, k, k) = ⟨π_{k}f_{1}⟩ and lenmid(f_{1}, k, k) = 1.

(28) mid(f_{1}, 0, 0) = f_{1}↾1.

(29) For all f_{1}, k such that lenf_{1} < k holds mid(f_{1}, k, k) = ε_{D}.

(30) For all f_{1}, i_{1}, i_{2} holds mid(f_{1}, i_{1}, i_{2}) = Rev(mid(f_{1}, i_{2}, i_{1})).

(31) Let f be a finite sequence of elements of E_{T}^{2} and given i_{1}, i_{2}, i. If 1 i_{1} and i_{1} < i_{2} and i_{2} lenf and 1 i and i < i_{2} − ′ i_{1} + 1, then L(mid(f, i_{1}, i_{2}), i) = L(f, (i + i_{1}) − ′1).

(32) Let f be a finite sequence of elements of E_{T}^{2} and given i_{1}, i_{2}, i. If 1 i_{1} and i_{1} < i_{2} and i_{2} lenf and 1 i and i < i_{2} − ′ i_{1} + 1, then L(mid(f, i_{2}, i_{1}), i) = L(f, i_{2} − ′i).

3. Dividing of special circular sequences into parts

Let n be a natural number and let f be a finite sequence. The functor S Drop(n, f) yields a natural number and is defined by:

(Def. 1) S Drop(n, f) = \{ \begin{matrix}n mod lenf − ′1, if n mod lenf − ′1 ≠ 0, \\ lenf − ′1, otherwise. \end{matrix}

Next we state three propositions:

(33) For every finite sequence f such that 0 < lenf − ′1 holds S Drop(lenf − ′ 1, f) = lenf − ′1.

(34) For every natural number n and for every finite sequence f such that 1 n and n lenf − ′1 holds S Drop(n, f) = n.

(35) Let n be a natural number and f be a finite sequence. If lenf > 1 or lenf − ′ 1 > 0, then S Drop(n, f) = S Drop(n + lenf − ′ 1, f) and S Drop(n, f) = S Drop(lenf − ′1 + n, f).

Let f be a non constant standard special circular sequence, let g be a finite sequence of elements of E_{T}^{2}, and let i_{1}, i_{2} be natural numbers. We say that g is a right part of f from i_{1} to i_{2} if and only if the conditions (Def. 2) are satisfied.

(Def. 2)(i) 1 i_{1}, (ii) i_{1} + 1 lenf, (iii) 1 i_{2}, (iv) i_{2} + 1 lenf,

(v) g(leng) = f(i_{2}), (vi) 1 leng, (vii) leng < lenf, and (viii) for every natural number i such that 1 i and i leng holds g(i) =

f(S Drop((i_{1} + i) − ′1, f)). Let f be a non constant standard special circular sequence, let g be a finite

sequence of elements of E_{T}^{2}, and let i_{1}, i_{2} be natural numbers. We say that g is a left part of f from i_{1} to i_{2} if and only if the conditions (Def. 3) are satisfied.

(Def. 3)(i) 1 i_{1}, (ii) i_{1} + 1 lenf, (iii) 1 i_{2}, (iv) i_{2} + 1 lenf,

(v) g(leng) = f(i_{2}), (vi) 1 leng, (vii) leng < lenf, and (viii) for every natural number i such that 1 i and i leng holds g(i) =

f(S Drop((lenf + i_{1}) − ′i, f)). Let f be a non constant standard special circular sequence, let g be a finite

sequence of elements of E_{T}^{2}, and let i_{1}, i_{2} be natural numbers. We say that g is a part of f from i_{1} to i_{2} if and only if:

(Def. 4) g is a right part of f from i_{1} to i_{2} or a left part of f from i_{1} to i_{2}.

We now state a number of propositions:

(36) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a part of f from i_{1} to i_{2}. Then

(i) 1 i_{1}, (ii) i_{1} + 1 lenf, (iii) 1 i_{2}, (iv) i_{2} + 1 lenf,

(v) g(leng) = f(i_{2}), (vi) 1 leng, (vii) leng < lenf, and (viii) for every natural number i such that 1 i and i leng holds g(i) =

f(S Drop((i_{1} + i) − ′1, f)) or for every natural number i such that 1 i and i leng holds g(i) = f(S Drop((lenf + i_{1}) − ′i, f)).

(37) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a right part of f from i_{1} to i_{2} and i_{1} i_{2}. Then leng = i_{2} − ′i_{1} + 1 and g = mid(f, i_{1}, i_{2}).

(38) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a right part of f from i_{1} to i_{2} and i_{1} > i_{2}. Then leng = (lenf + i_{2}) − ′i_{1} and g = (mid(f, i_{1}, lenf − ′1))^{⌢} (f↾i_{2}) and g = (mid(f, i_{1}, lenf − ′1))^{⌢} mid(f, 1, i_{2}).

(39) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a left part of f from i_{1} to i_{2} and i_{1} i_{2}. Then leng = i_{1} − ′i_{2} + 1 and g = mid(f, i_{1}, i_{2}).

(40) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a left part of f from i_{1} to i_{2} and i_{1} < i_{2}. Then leng = (lenf + i_{1}) − ′i_{2} and g = (mid(f, i_{1}, 1))^{⌢} mid(f, lenf − ′1, i_{2}).

(41) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a right part of f from i_{1} to i_{2}. Then Rev(g) is a left part of f from i_{2} to i_{1}.

(42) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a left part of f from i_{1} to i_{2}. Then Rev(g) is a right part of f from i_{2} to i_{1}.

(43) Let f be a non constant standard special circular sequence and i_{1}, i_{2} be natural numbers. If 1 i_{1} and i_{1} i_{2} and i_{2} < lenf, then mid(f, i_{1}, i_{2}) is a right part of f from i_{1} to i_{2}.

(44) Let f be a non constant standard special circular sequence and i_{1}, i_{2} be natural numbers. If 1 i_{1} and i_{1} i_{2} and i_{2} < lenf, then mid(f, i_{2}, i_{1}) is a left part of f from i_{2} to i_{1}.

(45) Let f be a non constant standard special circular sequence and i_{1}, i_{2} be natural numbers. Suppose 1 i_{2} and i_{1} > i_{2} and i_{1} < lenf. Then (mid(f, i_{1}, lenf − ′1))^{⌢} mid(f, 1, i_{2}) is a right part of f from i_{1} to i_{2}.

(46) Let f be a non constant standard special circular sequence and i_{1}, i_{2} be natural numbers. Suppose 1 i_{1} and i_{1} < i_{2} and i_{2} < lenf. Then (mid(f, i_{1}, 1))^{⌢} mid(f, lenf − ′1, i_{2}) is a left part of f from i_{1} to i_{2}.

(47) Let h be a finite sequence of elements of E_{T}^{2} and given i_{1}, i_{2}. If 1 i_{1} and i_{1} lenh and 1 i_{2} and i_{2} lenh, then L̃(mid(h, i_{1}, i_{2})) ⊆ L̃(h).

(48) Let g be a finite sequence of elements of D. Then g is one-to-one if and only if for all i_{1}, i_{2} such that 1 i_{1} and i_{1} leng and 1 i_{2} and i_{2} leng and g(i_{1}) = g(i_{2}) or π_{i_{1}}g = π_{i_{2}}g holds i_{1} = i_{2}.

(49) Let f be a non constant standard special circular sequence and given i_{2}. If 1 < i_{2} and i_{2} + 1 lenf, then f↾i_{2} is a special sequence.

(50) Let f be a non constant standard special circular sequence and given i_{2}. If 1 i_{2} and i_{2} + 1 < lenf, then f_{⇂i_{2}} is a special sequence.

(51) Let f be a non constant standard special circular sequence and given i_{1}, i_{2}. If 1 i_{1} and i_{1} < i_{2} and i_{2} + 1 lenf, then mid(f, i_{1}, i_{2}) is a special sequence.

(52) Let f be a non constant standard special circular sequence and given i_{1}, i_{2}. If 1 < i_{1} and i_{1} < i_{2} and i_{2} lenf, then mid(f, i_{1}, i_{2}) is a special sequence.

(53) For all points p_{0}, p, q_{1}, q_{2} of E_{T}^{2} such that p_{0} ∈ L(p, q_{1}) and p_{0} ∈ L(p, q_{2}) and p ≠ p_{0} holds q_{1} ∈ L(p, q_{2}) or q_{2} ∈ L(p, q_{1}).

(54) For every non constant standard special circular sequence f holds L(f, 1) ∩ L(f, lenf − ′1) = {f(1)}.

(55) Let f be a non constant standard special circular sequence, i_{1}, i_{2} be natural numbers, and g_{1}, g_{2} be finite sequences of elements of E_{T}^{2}. Suppose 1 i_{1} and i_{1} < i_{2} and i_{2} < lenf and g_{1} = mid(f, i_{1}, i_{2}) and g_{2} = (mid(f, i_{1}, 1))^{⌢} mid(f, lenf − ′1, i_{2}). Then L̃(g_{1}) ∩ L̃(g_{2}) = {f(i_{1}), f(i_{2})} and L̃(g_{1}) ∪ L̃(g_{2}) = L̃(f).

(56) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a right part of f from i_{1} to i_{2} and i_{1} < i_{2}. Then L̃(g) is a special polygonal arc joining π_{i_{1}}f and π_{i_{2}}f.

(57) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a left part of f from i_{1} to i_{2} and i_{1} > i_{2}. Then L̃(g) is a special polygonal arc joining π_{i_{1}}f and π_{i_{2}}f.

(58) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a right part of f from i_{1} to i_{2} and i_{1} ≠ i_{2}. Then L̃(g) is a special polygonal arc joining π_{i_{1}}f and π_{i_{2}}f.

(59) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a left part of f from i_{1} to i_{2} and i_{1} ≠ i_{2}. Then L̃(g) is a special polygonal arc joining π_{i_{1}}f and π_{i_{2}}f.

(60) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a part of f from i_{1} to i_{2} and i_{1} ≠ i_{2}. Then L̃(g) is a special polygonal arc joining π_{i_{1}}f and π_{i_{2}}f.

(61) Let f be a non constant standard special circular sequence, g be a finite sequence of elements of E_{T}^{2}, and i_{1}, i_{2} be natural numbers. Suppose g is a part of f from i_{1} to i_{2} and g(1) ≠ g(leng). Then L̃(g) is a special polygonal

arc joining π_{i_{1}}f and π_{i_{2}}f.

(62) Let f be a non constant standard special circular sequence and i_{1}, i_{2} be natural numbers. Suppose 1 i_{1} and i_{1} + 1 lenf and 1 i_{2} and i_{2} + 1 lenf and i_{1} ≠ i_{2}. Then there exist finite sequences g_{1}, g_{2} of elements of E_{T}^{2} such that

(i) g_{1} is a part of f from i_{1} to i_{2}, (ii) g_{2} is a part of f from i_{1} to i_{2}, (iii) L̃(g_{1}) ∩ L̃(g_{2}) = {f(i_{1}), f(i_{2})}, (iv) L̃(g_{1}) ∪ L̃(g_{2}) = L̃(f),

(v) L̃(g_{1}) is a special polygonal arc joining π_{i_{1}}f and π_{i_{2}}f, (vi) L̃(g_{2}) is a special polygonal arc joining π_{i_{1}}f and π_{i_{2}}f, and (vii) for every finite sequence g of elements of E_{T}^{2} such that g is a part of f

from i_{1} to i_{2} holds g = g_{1} or g = g_{2}.

In the sequel g_{1}, g_{2} are finite sequences of elements of E_{T}^{2}. We now state several propositions:

(63) Let f be a non constant standard special circular sequence and P be a non empty subset of the carrier of (E_{T}^{2}).If P = L̃(f), then P is a simple closed curve.

(64) Let f be a non constant standard special circular sequence and given g_{1}, g_{2}. Suppose g_{1} is a right part of f from i_{1} to i_{2} and g_{2} is a right part of f from i_{1} to i_{2}. Then g_{1} = g_{2}.

(65) Let f be a non constant standard special circular sequence and given g_{1}, g_{2}. Suppose g_{1} is a left part of f from i_{1} to i_{2} and g_{2} is a left part of f from i_{1} to i_{2}. Then g_{1} = g_{2}.

(66) Let f be a non constant standard special circular sequence and given g_{1}, g_{2}. Suppose i_{1} ≠ i_{2} and g_{1} is a right part of f from i_{1} to i_{2} and g_{2} is a left part of f from i_{1} to i_{2}. Then g_{1}(2) ≠ g_{2}(2).

(67) Let f be a non constant standard special circular sequence and given g_{1}, g_{2}. Suppose i_{1} ≠ i_{2} and g_{1} is a part of f from i_{1} to i_{2} and g_{2} is a part of f from i_{1} to i_{2} and g_{1}(2) = g_{2}(2). Then g_{1} = g_{2}.

Let f be a non constant standard special circular sequence and let i_{1}, i_{2} be natural numbers. Let us assume that 1 i_{1} and i_{1} + 1 lenf and 1 i_{2} and i_{2} + 1 lenf and i_{1} ≠ i_{2}. The functor Lower(f, i_{1}, i_{2}) yields a finite sequence of elements of E_{T}^{2} and is defined by the conditions (Def. 5).

(Def. 5)(i) Lower(f, i_{1}, i_{2}) is a part of f from i_{1} to i_{2},

(ii) if (π_{i_{1}+1}f)_{1} < (π_{i_{1}}f)_{1} or (π_{i_{1}+1}f)_{2} < (π_{i_{1}}f)_{2}, then (Lower(f, i_{1}, i_{2}))(2) =

f(i_{1} + 1), and (iii) if (π_{i_{1}+1}f)_{1} (π_{i_{1}}f)_{1} and (π_{i_{1}+1}f)_{2} (π_{i_{1}}f)_{2}, then

(Lower(f, i_{1}, i_{2}))(2) = f(S Drop(i_{1} − ′1, f)).

358 yatsuka nakamura et al.

The functor Upper(f, i_{1}, i_{2}) yielding a finite sequence of elements of E_{T}^{2} is defined by the conditions (Def. 6).

(Def. 6)(i) Upper(f, i_{1}, i_{2}) is a part of f from i_{1} to i_{2}, (ii) if (π_{i_{1}+1}f)_{1} > (π_{i_{1}}f)_{1} or (π_{i_{1}+1}f)_{2} > (π_{i_{1}}f)_{2}, then (Upper(f, i_{1}, i_{2}))(2) =

f(i_{1} + 1), and (iii) if (π_{i_{1}+1}f)_{1} (π_{i_{1}}f)_{1} and (π_{i_{1}+1}f)_{2} (π_{i_{1}}f)_{2}, then

(Upper(f, i_{1}, i_{2}))(2) = f(S Drop(i_{1} − ′1, f)).

References

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

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

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

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

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

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

[7] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Simple closed curves. Formalized Mathematics, 2(5):663–664, 1991.

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

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

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

[11] Yatsuka Nakamura and Jarosław Kotowicz. Connectedness conditions using polygonal arcs. Formalized Mathematics, 3(1):101–106, 1992.

[12] Yatsuka Nakamura and Roman Matuszewski. Reconstructions of special sequences. Formalized Mathematics, 6(2):255–263, 1997.

[13] Yatsuka Nakamura and Andrzej Trybulec. Decomposing a Go-board into cells. Formalized Mathematics, 5(3):323–328, 1996.

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

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

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

[17] Andrzej Trybulec. On the decomposition of finite sequences. Formalized Mathematics, 5(3):317–322, 1996.

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

[19] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

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

Lattice of Substitutions

Adam Grabowski Warsaw University Białystok

MML Identifier: SUBSTLAT.

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

1. Preliminaries

In this paper V, C are sets. Let us consider V, C. The functor SubstitutionSet(V, C) yielding a subset

of Fin(V ˙→ C) is defined as follows: (Def. 1) SubstitutionSet(V, C) = {A, A ranges over elements of Fin(V ˙→ C) :

⋀_{s,t: element of V ˙→ C} (s ∈ A ∧ t ∈ A ∧ s ⊆ t ⇒ s = t)}. Next we state two propositions:

(1) ∅ ∈ SubstitutionSet(V, C).

(2) {∅} ∈ SubstitutionSet(V, C). Let us consider V, C. One can check that SubstitutionSet(V, C) is non empty. Let us consider V, C and let A, B be elements of SubstitutionSet(V, C).

Then A ∪ B is an element of Fin(V ˙→ C).

Let us consider V, C. Note that there exists an element of SubstitutionSet(V, C) which is non empty.

Let us consider V, C. Note that every element of SubstitutionSet(V, C) is finite.

Let us consider V, C and let A be an element of Fin(V ˙→ C). The functor □^{c}_{A} yields an element of SubstitutionSet(V, C) and is defined by:

(Def. 2) □^{c}_{A} = {t, t ranges over elements of V ˙→ C : ⋀_{s: element of V ˙→ C} (s ∈ A ∧ s ⊆ t ⇔ s = t)}.

Let us consider V, C and let A be a non empty element of SubstitutionSet(V, C). Note that every element of A is function-like and relation-like.

Let us consider V, C. One can verify that every element of V ˙→ C is functionlike and relation-like.

Let us consider V, C and let A, B be elements of Fin(V ˙→ C). The functor A^{⌢} B yields an element of Fin(V ˙→ C) and is defined as follows:

(Def. 3) A^{⌢} B = {s ∪ t, s ranges over elements of V ˙→ C, t ranges over elements

of V ˙→ C : s ∈ A ∧ t ∈ B ∧ s ≈ t}. In the sequel A, B, D are elements of Fin(V ˙→ C). One can prove the following propositions:

(3) A^{⌢} B = B ^{⌢} A.

(4) If B = {∅}, then A^{⌢} B = A.

(5) For all sets a, b such that B ∈ SubstitutionSet(V, C) and a ∈ B and b ∈ B and a ⊆ b holds a = b.

(6) For every set a such that a ∈ □^{c}_{B} holds a ∈ B and for every set b such that b ∈ B and b ⊆ a holds b = a.

(7) For every set a such that a ∈ B and for every set b such that b ∈ B and b ⊆ a holds b = a holds a ∈ □^{c}_{B}.

(8) □^{c}_{A} ⊆ A.

(9) If A = ∅, then □^{c}_{A} = ∅.

(10) For every set b such that b ∈ B there exists a set c such that c ⊆ b and c ∈ □^{c}_{B}.

(11) For every element K of SubstitutionSet(V, C) holds □^{c}_{K} = K.

(12) □^{c}_{A∪B} ⊆ □^{c}_{A} ∪ B.

(13) □^{c}_{□^{c}_{A}∪B} = □^{c}_{A∪B} .

(14) If A ⊆ B, then A^{⌢} D ⊆ B ^{⌢} D.

(15) For every set a such that a ∈ A^{⌢} B there exist sets b, c such that b ∈ A and c ∈ B and a = b ∪ c.

(16) For all elements b, c of V ˙→ C such that b ∈ A and c ∈ B and b ≈ c holds b ∪ c ∈ A^{⌢} B.

(17) □^{c}_{A^{⌢}B} ⊆ (□^{c}_{A})^{⌢} B.

(18) If A ⊆ B, then D^{⌢} A ⊆ D^{⌢} B.

(19) □^{c}_{(□^{c}_{A})^{⌢}B} = □^{c}_{A^{⌢}B}.

(20) □^{c}_{A^{⌢}(□^{c}_{B})} = □^{c}_{A^{⌢}B}.

(21) For all elements K, L, M of Fin(V ˙→ C) holds K^{⌢}(L^{⌢}M) = (K^{⌢}L)^{⌢}M.

(22) For all elements K, L, M of Fin(V ˙→ C) holds K ^{⌢} (L ∪ M) = K ^{⌢} L ∪ K ^{⌢} M.

(23) B ⊆ B ^{⌢} B.

lattice of substitutions 361

(24) □^{c}_{A^{⌢}A} = □^{c}_{A}.

(25) For every element K of SubstitutionSet(V, C) holds □^{c}_{K^{⌢}K} = K.

2. Definition of the lattice

Let us consider V, C. The functor SubstLatt(V, C) yielding a strict lattice structure is defined by the conditions (Def. 4).

(Def. 4)(i) The carrier of SubstLatt(V, C) = SubstitutionSet(V, C), and (ii) for all elements A, B of SubstitutionSet(V, C) holds (the join ope-

ration of SubstLatt(V, C))(A, B) = □^{c}_{A∪B} and (the meet operation of SubstLatt(V, C))(A, B) = □^{c}_{A^{⌢}B}.

Let us consider V, C. One can verify that SubstLatt(V, C) is non empty. Let us consider V, C. Note that SubstLatt(V, C) is lattice-like. Let us consider V, C. Observe that SubstLatt(V, C) is distributive and bo-

unded.

One can prove the following two propositions:

(26) ⊥_{SubstLatt (V,C)} = ∅.

(27) ⊤_{SubstLatt (V,C)} = {∅}.

References

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

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

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

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

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

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

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

[8] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

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

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

[11] Stanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215– 222, 1990.

362 adam grabowski

Equations in Many Sorted Algebras

Artur Korniłowicz Warsaw University Białystok

Summary. This paper is preparation to prove Birkhoff’s Theorem. Some properties of many sorted algebras are proved. The last section of this work shows that every equation valid in a many sorted algebra is also valid in each subalgebra, and each image of it. Moreover for a family of many sorted algebras (A_{i} : i ∈ I) if every equation is valid in each A_{i}, i ∈ I then is also valid in product ∏(A_{i} : i ∈ I).

MML Identifier: EQUATION.

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

1. On the Functions and Many Sorted Functions

In this paper I is a set. Next we state several propositions:

(1) Let A be a set, B, C be non empty sets, f be a function from A into B, and g be a function from B into C. If rng(g · f) = C, then rngg = C.

(2) Let A be a many sorted set indexed by I, B, C be non-empty many sorted sets indexed by I, f be a many sorted function from A into B, and g be a many sorted function from B into C. If g ∘ f is onto, then g is onto.

(3) Let A, B be non empty sets, C, y be sets, and f be a function. If f ∈ (C^{B})^{A} and y ∈ B, then dom(commute(f))(y) = A and rng(commute(f))(y) ⊆ C.

(4) For every many sorted set A indexed by I there exists a non-empty many sorted set B indexed by I such that A ⊆ B.

(5) Let A, B be many sorted sets indexed by I. Suppose A is transformable to B. Let f be a many sorted function indexed by I. If dom_{κ} f(κ) = A and rng_{κ} f(κ) ⊆ B, then f is a many sorted function from A into B.

(6) Let A, B be many sorted sets indexed by I, F be a many sorted function from A into B, C, E be many sorted subsets indexed by A, and D be a many sorted subset indexed by C. If E = D, then F ↾ C ↾ D = F ↾ E.

(7) Let B be a non-empty many sorted set indexed by I, C be a many sorted set indexed by I, A be a many sorted subset indexed by C, and F be a many sorted function from A into B. Then there exists a many sorted function G from C into B such that G ↾ A = F.

Let I be a set, let A be a many sorted set indexed by I, and let F be a many sorted function indexed by I. The functor F^{−1} (A) yielding a many sorted set indexed by I is defined as follows:

(Def. 1) For every set i such that i ∈ I holds (F^{−1} (A))(i) = F (i)^{−1} (A(i)). We now state a number of propositions:

(8) Let A, B, C be many sorted sets indexed by I and F be a many sorted function from A into B. Then F ^{∘} C is a many sorted subset indexed by B.

(9) Let A, B, C be many sorted sets indexed by I and F be a many sorted function from A into B. Then F^{−1} (C) is a many sorted subset indexed by A.

(10) Let A, B be many sorted sets indexed by I and F be a many sorted function from A into B. If F is onto, then F ^{∘} A = B.

(11) Let A, B be many sorted sets indexed by I and F be a many sorted function from A into B. If A is transformable to B, then F^{−1} (B) = A.

(12) Let A be a many sorted set indexed by I and F be a many sorted function indexed by I. If A ⊆ rng_{κ} F (κ), then F ^{∘} F^{−1} (A) = A.

(13) For every many sorted function f indexed by I and for every many sorted set X indexed by I holds f ^{∘} X ⊆ rng_{κ} f(κ).

(14) For every many sorted function f indexed by I holds f ^{∘} (dom_{κ} f(κ)) = rng_{κ} f(κ).

(15) For every many sorted function f indexed by I holds f^{−1} (rng_{κ} f(κ)) = dom_{κ} f(κ).

(16) For every many sorted set A indexed by I holds (id_{A})^{∘} A = A.

(17) For every many sorted set A indexed by I holds (id_{A})^{−1} (A) = A.

2. On the Many Sorted Algebras

In the sequel S denotes a non empty non void many sorted signature and U_{0}, U_{1} denote non-empty algebras over S.

One can prove the following propositions:

(18) For every algebra A over S holds the algebra of A is a subalgebra of A.

(19) Every algebra A over S is a subalgebra of the algebra of A.

(20) Let U_{0} be an algebra over S, A be a subalgebra of U_{0}, o be an operation symbol of S, and x be a set. If x ∈ Args(o, A), then x ∈ Args(o, U_{0}).

(21) Let U_{0} be an algebra over S, A be a subalgebra of U_{0}, o be an operation symbol of S, and x be a set. If x ∈ Args(o, A), then (Den(o, A))(x) = (Den(o, U_{0}))(x).

(22) Let F be an algebra family of I over S, B be a subalgebra of ∏ F, o be an operation symbol of S, and x be a set. If x ∈ Args(o, B), then (Den(o, B))(x) is a function and (Den(o, ∏ F))(x) is a function.

Let S be a non void non empty many sorted signature, let A be an algebra over S, and let B be a subalgebra of A. The functor SuperAlgebraSet(B) is defined by the condition (Def. 2).

(Def. 2) Let x be a set. Then x ∈ SuperAlgebraSet(B) if and only if there exists

a strict subalgebra C of A such that x = C and B is a subalgebra of C. Let S be a non void non empty many sorted signature, let A be an algebra

over S, and let B be a subalgebra of A. Note that SuperAlgebraSet(B) is non empty.

Let S be a non empty non void many sorted signature. One can verify that there exists an algebra over S which is strict, non-empty, and free.

Let S be a non empty non void many sorted signature, let A be a non-empty algebra over S, and let X be a non-empty locally-finite subset of A. One can verify that Gen(X) is finitely-generated.

Let S be a non empty non void many sorted signature and let A be a nonempty algebra over S. Note that there exists a subalgebra of A which is strict, non-empty, and finitely-generated.

Let S be a non empty non void many sorted signature and let A be a feasible algebra over S. Note that there exists a subalgebra of A which is feasible.

Next we state several propositions:

(23) Let A be an algebra over S, C be a subalgebra of A, and D be a many sorted subset indexed by the sorts of A. Suppose D = the sorts of C. Let h be a many sorted function from A into U_{0} and g be a many sorted function from C into U_{0}. Suppose g = h ↾ D. Let o be an operation symbol of S, x be an element of Args(o, A), and y be an element of Args(o, C). If Args(o, C) ≠ ∅ and x = y, then h#x = g#y.

(24) Let A be a feasible algebra over S, C be a feasible subalgebra of A, and D be a many sorted subset indexed by the sorts of A. Suppose D = the sorts of C. Let h be a many sorted function from A into U_{0}. Suppose h is a homomorphism of A into U_{0}. Let g be a many sorted function from C into U_{0}. If g = h ↾ D, then g is a homomorphism of C into U_{0}.

(25) Let B be a strict non-empty algebra over S, G be a generator set of U_{0}, H be a non-empty generator set of B, and f be a many sorted function from U_{0} into B. Suppose H ⊆ f ^{∘} G and f is a homomorphism of U_{0} into B. Then f is an epimorphism of U_{0} onto B.

(26) Let W be a strict free non-empty algebra over S and F be a many sorted function from U_{0} into U_{1}. Suppose F is an epimorphism of U_{0} onto U_{1}. Let G be a many sorted function from W into U_{1}. Suppose G is a homomorphism of W into U_{1}. Then there exists a many sorted function H from W into U_{0} such that H is a homomorphism of W into U_{0} and G = F ∘ H.

(27) Let I be a non empty finite set, A be a non-empty algebra over S, and F be an algebra family of I over S. Suppose that for every element i of I there exists a strict non-empty finitely-generated subalgebra C of A such that C = F (i). Then there exists a strict non-empty finitely-generated subalgebra B of A such that for every element i of I holds F (i) is a subalgebra of B.

(28) Let A, B be strict non-empty finitely-generated subalgebras of U_{0}. Then there exists a strict non-empty finitely-generated subalgebra M of U_{0} such that A is a subalgebra of M and B is a subalgebra of M.

(29) Let S_{1} be a non empty non void many sorted signature, A_{1} be a nonempty algebra over S_{1}, and C be a set. Suppose C = {A, A ranges over elements of Subalgebras(A_{1}): ⋁_{R: strict non-empty finitely-generated subalgebra of A_{1}} R = A}. Let F be an algebra family of C over S_{1}. Suppose that for every set c such that c ∈ C holds c = F (c). Then there exists a strict non-empty subalgebra P_{1} of ∏ F such that there exists a many sorted function from P_{1} into A_{1} which is an epimorphism of P_{1} onto A_{1}.

(30) Let U_{0} be a feasible free algebra over S, A be a free generator set of U_{0}, and Z be a subset of U_{0}. If Z ⊆ A and Gen(Z) is feasible, then Gen(Z) is free.

3. Equations in Many Sorted Algebras

Let S be a non empty non void many sorted signature. The functor T_{S}(ℕ) yielding an algebra over S is defined by:

(Def. 3) T_{S}(ℕ) = Free((the carrier of S) ⟼→ ℕ).

Let S be a non empty non void many sorted signature. Note that T_{S}(ℕ) is strict non-empty and free.

Let S be a non empty non void many sorted signature. The equations of S constitute a many sorted set indexed by the carrier of S and is defined by:

(Def. 4) The equations of S = [[the sorts of T_{S}(ℕ), the sorts of T_{S}(ℕ)]].

Let S be a non empty non void many sorted signature. Observe that the equations of S is non-empty.

Let S be a non empty non void many sorted signature. A set of equations of S is a many sorted subset indexed by the equations of S.

In the sequel s denotes a sort symbol of S, e denotes an element of (the equations of S)(s), and E denotes a set of equations of S.

Let S be a non empty non void many sorted signature, let s be a sort symbol of S, and let x, y be elements of (the sorts of T_{S}(ℕ))(s). Then ⟨⟨x, y⟩⟩ is an element of (the equations of S)(s). We introduce x= y as a synonym of ⟨⟨x, y⟩⟩.

Next we state two propositions:

(31) e_{1} ∈ (the sorts of T_{S}(ℕ))(s).

(32) e_{2} ∈ (the sorts of T_{S}(ℕ))(s).

Let S be a non empty non void many sorted signature, let A be an algebra over S, let s be a sort symbol of S, and let e be an element of (the equations of S)(s). The predicate A ⊧ e is defined by:

(Def. 5) For every many sorted function h from T_{S}(ℕ) into A such that h is a

homomorphism of T_{S}(ℕ) into A holds h(s)(e_{1}) = h(s)(e_{2}). Let S be a non empty non void many sorted signature, let A be an algebra

over S, and let E be a set of equations of S. The predicate A ⊧ E is defined as follows:

(Def. 6) For every sort symbol s of S and for every element e of (the equations

of S)(s) such that e ∈ E(s) holds A ⊧ e. We now state several propositions:

(33) For every strict non-empty subalgebra U_{2} of U_{0} such that U_{0} ⊧ e holds U_{2} ⊧ e.

(34) For every strict non-empty subalgebra U_{2} of U_{0} such that U_{0} ⊧ E holds U_{2} ⊧ E.

(35) If U_{0} and U_{1} are isomorphic and U_{0} ⊧ e, then U_{1} ⊧ e.

(36) If U_{0} and U_{1} are isomorphic and U_{0} ⊧ E, then U_{1} ⊧ E.

(37) For every congruence R of U_{0} such that U_{0} ⊧ e holds U_{0}/R ⊧ e.

(38) For every congruence R of U_{0} such that U_{0} ⊧ E holds U_{0}/R ⊧ E.

368 artur korniłowicz

(39) Let F be an algebra family of I over S. Suppose that for every set i such that i ∈ I there exists an algebra A over S such that A = F (i) and A ⊧ e. Then ∏ F ⊧ e.

(40) Let F be an algebra family of I over S. Suppose that for every set i such that i ∈ I there exists an algebra A over S such that A = F (i) and A ⊧ E. Then ∏ F ⊧ E.

References

[1] Grzegorz Bancerek. Curried and uncurried functions. Formalized Mathematics, 1(3):537– 541, 1990.

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

[3] Grzegorz Bancerek. Translations, endomorphisms, and stable equational theories. Formalized Mathematics, 5(4):553–564, 1996.

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

[5] Ewa Burakowska. Subalgebras of many sorted algebra. Lattice of subalgebras. Formalized Mathematics, 5(1):47–54, 1996.

[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. The modification of a function by a function and the iteration of the composition of a function. Formalized Mathematics, 1(3):521–527, 1990.

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

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

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

[12] Mariusz Giero. More on products of many sorted algebras. Formalized Mathematics, 5(4):621–626, 1996.

[13] Artur Korniłowicz. Extensions of mappings on generator set. Formalized Mathematics, 5(2):269–272, 1996.

[14] Artur Korniłowicz. On the closure operator and the closure system of many sorted sets. Formalized Mathematics, 5(4):543–551, 1996.

[15] Artur Korniłowicz. On the group of automorphisms of universal algebra & many sorted algebra. Formalized Mathematics, 5(2):221–226, 1996.

[16] Małgorzata Korolkiewicz. Homomorphisms of many sorted algebras. Formalized Mathematics, 5(1):61–65, 1996.

[17] Małgorzata Korolkiewicz. Many sorted quotient algebra. Formalized Mathematics, 5(1):79–84, 1996.

[18] Beata Madras. Product of family of universal algebras. Formalized Mathematics, 4(1):103– 108, 1993.

[19] Beata Madras. Products of many sorted algebras. Formalized Mathematics, 5(1):55–60, 1996.

[20] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Formalized Mathematics, 5(2):167–172, 1996.

[21] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, II. Formalized Mathematics, 5(2):215–220, 1996.

[22] Beata Perkowska. Free many sorted universal algebra. Formalized Mathematics, 5(1):67– 74, 1996.

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

[24] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

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

[26] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37–42, 1996.

equations in many sorted algebras 369

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

[28] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

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

370 artur korniłowicz

Category of Functors Between Alternative Categories

Robert Nieszczerzewski Warsaw University Białystok

MML Identifier: FUNCTOR2.

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

1. Preliminaries

Let A be a transitive non empty category structure with units and let B be a non empty category structure with units. Observe that every functor from A to B is feasible and id-preserving.

Let A be a transitive non empty category structure with units and let B be a non empty category structure with units. One can check the following observations:

∗ every functor from A to B which is covariant is also precovariant and comp-preserving,

∗ every functor from A to B which is precovariant and comp-preserving is also covariant,

∗ every functor from A to B which is contravariant is also precontravariant and comp-reversing, and

∗ every functor from A to B which is precontravariant and comp-reversing is also contravariant.

The following proposition is true (2)^{1} Let A, B be transitive non empty category structures with units, F be

a covariant functor from A to B, and a be an object of A. Then F (id_{a}) = id_{F (a)} .

2. Transformations

Let A, B be transitive non empty category structures with units and let F_{1}, F_{2} be covariant functors from A to B. We say that F_{1} is transformable to F_{2} if and only if:

(Def. 1) For every object a of A holds ⟨F_{1}(a), F_{2}(a)⟩ ≠ ∅.

Let us note that the predicate F_{1} is transformable to F_{2} is reflexive. One can prove the following proposition (4)^{2} Let A, B be transitive non empty category structures with units and

F, F_{1}, F_{2} be covariant functors from A to B. Suppose F is transformable to F_{1} and F_{1} is transformable to F_{2}. Then F is transformable to F_{2}.

Let A, B be transitive non empty category structures with units and let F_{1}, F_{2} be covariant functors from A to B. Let us assume that F_{1} is transformable to F_{2}. A many sorted set indexed by the carrier of A is said to be a transformation from F_{1} to F_{2} if:

(Def. 2) For every object a of A holds it(a) is a morphism from F_{1}(a) to F_{2}(a).

Let A, B be transitive non empty category structures with units and let F be a covariant functor from A to B. The functor id_{F} yielding a transformation from F to F is defined by:

(Def. 3) For every object a of A holds id_{F} (a) = id_{F (a)} .

Let A, B be transitive non empty category structures with units and let F_{1}, F_{2} be covariant functors from A to B. Let us assume that F_{1} is transformable to F_{2}. Let t be a transformation from F_{1} to F_{2} and let a be an object of A. The functor t[a] yielding a morphism from F_{1}(a) to F_{2}(a) is defined as follows:

(Def. 4) t[a] = t(a).

Let A, B be transitive non empty category structures with units and let F, F_{1}, F_{2} be covariant functors from A to B. Let us assume that F is transformable to F_{1} and F_{1} is transformable to F_{2}. Let t_{1} be a transformation from F to F_{1} and let t_{2} be a transformation from F_{1} to F_{2}. The functor t_{2} ^{∘} t_{1} yielding a transformation from F to F_{2} is defined by:

(Def. 5) For every object a of A holds (t_{2} ^{∘} t_{1})[a] = t_{2}[a] · t_{1}[a].

We now state four propositions:

1The proposition (1) has been removed.

2The proposition (3) has been removed.

(5) Let A, B be transitive non empty category structures with units and F_{1}, F_{2} be covariant functors from A to B. Suppose F_{1} is transformable to F_{2}. Let t_{1}, t_{2} be transformations from F_{1} to F_{2}. If for every object a of A holds t_{1}[a] = t_{2}[a], then t_{1} = t_{2}.

(6) Let A, B be transitive non empty category structures with units, F be a covariant functor from A to B, and a be an object of A. Then id_{F} [a] = id_{F (a)} .

(7) Let A, B be transitive non empty category structures with units and F_{1}, F_{2} be covariant functors from A to B. Suppose F_{1} is transformable to F_{2}. Let t be a transformation from F_{1} to F_{2}. Then id_{(F_{2})} ^{∘}t = t and t^{∘} id_{(F_{1})} = t.

(8) Let A, B be categories and F, F_{1}, F_{2}, F_{3} be covariant functors from A to B. Suppose F is transformable to F_{1} and F_{1} is transformable to F_{2} and F_{2} is transformable to F_{3}. Let t_{1} be a transformation from F to F_{1}, t_{2} be a transformation from F_{1} to F_{2}, and t_{3} be a transformation from F_{2} to F_{3}. Then (t_{3} ^{∘} t_{2})^{∘} t_{1} = t_{3} ^{∘} (t_{2} ^{∘} t_{1}).

3. Natural Transformations

Let A, B be transitive non empty category structures with units and let F_{1}, F_{2} be covariant functors from A to B. We say that F_{1} is naturally transformable to F_{2} if and only if the conditions (Def. 6) are satisfied.

(Def. 6)(i) F_{1} is transformable to F_{2}, and

(ii) there exists a transformation t from F_{1} to F_{2} such that for all objects a, b of A such that ⟨a, b⟩ ≠ ∅ and for every morphism f from a to b holds t[b] · F_{1}(f) = F_{2}(f) · t[a].

We now state two propositions:

(9) For all transitive non empty category structures A, B with units holds every covariant functor F from A to B is naturally transformable to F.

(10) Let A, B be categories and F, F_{1}, F_{2} be covariant functors from A to B. Suppose F is naturally transformable to F_{1} and F_{1} is naturally transformable to F_{2}. Then F is naturally transformable to F_{2}.

Let A, B be transitive non empty category structures with units and let F_{1}, F_{2} be covariant functors from A to B. Let us assume that F_{1} is naturally transformable to F_{2}. A transformation from F_{1} to F_{2} is called a natural transformation from F_{1} to F_{2} if:

(Def. 7) For all objects a, b of A such that ⟨a, b⟩ ≠ ∅ and for every morphism f from a to b holds it [b] · F_{1}(f) = F_{2}(f) · it[a].

Let A, B be transitive non empty category structures with units and let F be a covariant functor from A to B. Then id_{F} is a natural transformation from F to F.

Let A, B be categories and let F, F_{1}, F_{2} be covariant functors from A to B. Let us assume that F is naturally transformable to F_{1} and F_{1} is naturally transformable to F_{2}. Let t_{1} be a natural transformation from F to F_{1} and let t_{2} be a natural transformation from F_{1} to F_{2}. The functor t_{2}^{∘} t_{1} yielding a natural transformation from F to F_{2} is defined by:

(Def. 8) t_{2} ^{∘} t_{1} = t_{2} ^{∘} t_{1}.

We now state three propositions:

(11) Let A, B be transitive non empty category structures with units and F_{1}, F_{2} be covariant functors from A to B. Suppose F_{1} is naturally transformable to F_{2}. Let t be a natural transformation from F_{1} to F_{2}. Then id_{(F_{2})} ^{∘}t = t and t^{∘} id_{(F_{1})} = t.

(12) Let A, B be transitive non empty category structures with units and F, F_{1}, F_{2} be covariant functors from A to B. Suppose F is naturally transformable to F_{1} and F_{1} is naturally transformable to F_{2}. Let t_{1} be a natural transformation from F to F_{1}, t_{2} be a natural transformation from F_{1} to F_{2}, and a be an object of A. Then (t_{2} ^{∘} t_{1})[a] = t_{2}[a] · t_{1}[a].

(13) Let A, B be categories, F, F_{1}, F_{2}, F_{3} be covariant functors from A to B, t be a natural transformation from F to F_{1}, and t_{1} be a natural transformation from F_{1} to F_{2}. Suppose F is naturally transformable to F_{1} and F_{1} is naturally transformable to F_{2} and F_{2} is naturally transformable to F_{3}. Let t_{3} be a natural transformation from F_{2} to F_{3}. Then (t_{3}^{∘} t_{1})^{∘} t = t_{3} ^{∘} (t_{1} ^{∘} t).

4. Category of Functors

Let I be a set and let A, B be many sorted sets indexed by I. The functor B^{A} yields a set and is defined as follows:

(Def. 9)(i) For every set x holds x ∈ B^{A} iff x is a many sorted function from A

into B if for every set i such that i ∈ I holds if B(i) = ∅, then A(i) = ∅, (ii) B^{A} = ∅, otherwise. Let A, B be transitive non empty category structures with units. The functor

Funct(A, B) yields a set and is defined as follows: (Def. 10) For every set x holds x ∈ Funct(A, B) iff x is a covariant strict functor

from A to B. Let A, B be categories. The functor B^{A} yields a strict non empty transitive

category structure and is defined by the conditions (Def. 11).

category of functors between alternative … 375

(Def. 11)(i) The carrier of B^{A} = Funct(A, B), (ii) for all strict covariant functors F, G from A to B and for every set x

holds x ∈ (the arrows of B^{A})(F, G) iff F is naturally transformable to G and x is a natural transformation from F to G, and

(iii) for all strict covariant functors F, G, H from A to B such that F is naturally transformable to G and G is naturally transformable to H and for every natural transformation t_{1} from F to G and for every natural transformation t_{2} from G to H there exists a function f such that f = (the composition of B^{A})(F, G, H) and f(t_{2}, t_{1}) = t_{2} ^{∘} t_{1}.

References

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

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

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

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

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

[6] Michał Muzalewski and Wojciech Skaba. Three-argument operations and four-argument operations. Formalized Mathematics, 2(2):221–224, 1991.

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

[8] Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1(3):495–500, 1990.

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

[10] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

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

[12] Andrzej Trybulec. Categories without uniqueness of cod and dom. Formalized Mathematics, 5(2):259–267, 1996.

[13] Andrzej Trybulec. Functors for alternative categories. Formalized Mathematics, 5(4):595– 608, 1996.

[14] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37–42, 1996.

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

376 robert nieszczerzewski

Yoneda Embedding

Mirosław Wojciechowski Warsaw University Białystok

MML Identifier: YONEDA 1.

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

In this paper A is a category, a is an object of A, and f is a morphism of A. Let us consider A. The functor EnsHomA yields a category and is defined

by: (Def. 1) EnsHomA = Ens_{Hom(A)} .

Next we state two propositions:

(1) Let f, g be functions and m_{1}, m_{2} be morphisms of EnsHomA. If codm_{1} = domm_{2} and ⟨⟨⟨⟨domm_{1}, codm_{1}⟩⟩, f⟩⟩ = m_{1} and ⟨⟨⟨⟨domm_{2}, codm_{2}⟩⟩, g⟩⟩= m_{2}, then ⟨⟨⟨⟨domm_{1}, codm_{2}⟩⟩, g · f⟩⟩= m_{2} · m_{1}.

(2) hom(a, − ) is a functor from A to EnsHomA. Let us consider A, a. The functor hom^{F}(a, − ) yields a functor from A to

EnsHomA and is defined by: (Def. 2) hom^{F}(a, − ) = hom(a, − ).

One can prove the following proposition

(3) For every morphism f of A holds hom^{F}(codf, − ) is naturally transformable to hom^{F}(domf, − ).

Let us consider A, f. The functor hom^{F}(f, − ) yields a natural transformation from hom^{F}(codf, − ) to hom^{F}(domf, − ) and is defined by:

(Def. 3) For every object o of A holds (hom^{F}(f, − ))(o) = ⟨⟨⟨⟨hom(codf, o),

hom(domf, o)⟩⟩, hom(f, id_{o})⟩⟩. Next we state the proposition (4) For every element f of the morphisms of A holds ⟨⟨⟨⟨hom^{F}(codf, − ),

hom^{F}(domf, − )⟩⟩, hom^{F}(f, − )⟩⟩ is an element of the morphisms of (EnsHomA)^{A}.

Let us consider A. The functor YonedaA yielding a contravariant functor from A into (EnsHomA)^{A} is defined by:

(Def. 4) For every morphism f of A holds (YonedaA)(f) = ⟨⟨⟨⟨hom^{F}(codf, − ),

hom^{F}(domf, − )⟩⟩, hom^{F}(f, − )⟩⟩. Let A, B be categories, let F be a contravariant functor from A into B, and

let c be an object of A. The functor F (c) yields an object of B and is defined as follows:

(Def. 5) F (c) = (ObjF)(c).

Next we state the proposition

(5) For every functor F from A to (EnsHomA)^{A} such that ObjF is one-to-one and F is faithful holds F is one-to-one.

Let C, D be categories and let T be a contravariant functor from C into D. We say that T is faithful if and only if:

(Def. 6) For all objects c, c′ of C such that hom(c, c′) ≠ ∅ and for all morphisms

f_{1}, f_{2} from c to c′ such that T (f_{1}) = T (f_{2}) holds f_{1} = f_{2}. The following three propositions are true:

(6) Let F be a contravariant functor from A into (EnsHomA)^{A}. If ObjF is one-to-one and F is faithful, then F is one-to-one.

(7) YonedaA is faithful.

(8) YonedaA is one-to-one. Let C, D be categories and let T be a contravariant functor from C into D.

We say that T is full if and only if the condition (Def. 7) is satisfied. (Def. 7) Let c, c′ be objects of C. Suppose hom(T (c′), T (c)) ≠ ∅. Let g be a

morphism from T (c′) to T (c). Then hom(c, c′) ≠ ∅ and there exists a morphism f from c to c′ such that g = T (f).

The following proposition is true

(9) YonedaA is full.

References

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

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

[3] Czesław Byliński. Introduction to categories and functors. Formalized Mathematics, 1(2):409–420, 1990.

[4] Czesław Byliński. Subcategories and products of categories. Formalized Mathematics, 1(4):725–732, 1990.

[5] Czesław Byliński. Category Ens. Formalized Mathematics, 2(4):527–533, 1991.

yoneda embedding 379

[6] Czesław Byliński. Opposite categories and contravariant functors. Formalized Mathematics, 2(3):419–424, 1991.

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

[8] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

[9] Andrzej Trybulec. Natural transformations. Discrete categories. Formalized Mathematics, 2(4):467–474, 1991.

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

380 mirosław wojciechowski

The Correctness of the Generic Algorithms of Brown and Henrici

Concerning Addition and Multiplication in Fraction Fields

Christoph Schwarzweller University of Tübingen Tübingen

Summary. We prove the correctness of the generic algorithms of Brown and Henrici concerning addition and multiplication in fraction fields of gcddomains. For that we first prove some basic facts about divisibility in integral domains and introduce the concept of amplesets. After that we are able to define gcd-domains and to prove the theorems of Brown and Henrici which are crucial for the correctness of the algorithms. In the last section we define Mizar functions mirroring their input/output behaviour and prove properties of these functions that ensure the correctness of the algorithms.

MML Identifier: GCD 1.

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

1. Basics

In this paper R denotes an integral domain and a, b, c denote elements of the carrier of R.

The following proposition is true

(1) For all elements a, b, c of the carrier of R such that a ≠ 0_{R} holds if a · b = a · c, then b = c and if b · a = c · a, then b = c.

Let R be an integral domain and let x, y be elements of the carrier of R. We say that x divides y if and only if:

(Def. 1) There exists an element z of the carrier of R such that y = x · z.

Let us notice that the predicate x divides y is reflexive.

Let R be an integral domain and let x be an element of the carrier of R. We say that x is unital if and only if:

(Def. 2) x divides 1_{R}.

Let R be an integral domain and let x, y be elements of the carrier of R. We say that x is associated to y if and only if:

(Def. 3) x divides y and y divides x.

Let us observe that the predicate x is associated to y is reflexive and symmetric. We introduce x is not associated to y as an antonym of x is associated to y.

Let R be an integral domain and let x, y be elements of the carrier of R. Let us assume that y divides x. And let us assume that y ≠ 0_{R}. The functor \frac{x}{y} yielding an element of the carrier of R is defined as follows:

(Def. 4) \frac{x}{y} · y = x.

One can prove the following propositions:

(2) For all elements a, b, c of the carrier of R such that a divides b and b divides c holds a divides c.

(3) Let a, b, c, d be elements of the carrier of R. If b divides a and d divides c, then b · d divides a · c.

(4) Let a, b, c be elements of the carrier of R. If a is associated to b and b is associated to c, then a is associated to c.

(5) For all elements a, b, c of the carrier of R such that a divides b holds c · a divides c · b.

(6) For all elements a, b of the carrier of R holds a divides a · b and b divides a · b.

(7) For all elements a, b, c of the carrier of R such that a divides b holds a divides b · c.

(8) Let a, b be elements of the carrier of R. If b divides a and b ≠ 0_{R}, then \frac{a}{b} = 0_{R} iff a = 0_{R}.

(9) For every element a of the carrier of R such that a ≠ 0_{R} holds \frac{a}{a} = 1_{R}.

(10) For every element a of the carrier of R holds \frac{a}{1_{R}} = a.

(11) Let a, b, c be elements of the carrier of R such that c ≠ 0_{R}. Then (i) if c divides a · b and c divides a, then \frac{a·b}{c} = \frac{a}{c} · b, and (ii) if c divides a · b and c divides b, then \frac{a·b}{c} = a · \frac{b}{c}.

(12) Let a, b, c be elements of the carrier of R. Suppose c ≠ 0_{R} and c divides a and c divides b and c divides a + b. Then \frac{a}{c} + \frac{b}{c} = \frac{a+b}{c}.

(13) Let a, b, c be elements of the carrier of R. Suppose c ≠ 0_{R} and c divides a and c divides b. Then \frac{a}{c} = \frac{b}{c} if and only if a = b.

(14) Let a, b, c, d be elements of the carrier of R. Suppose b ≠ 0_{R} and d ≠ 0_{R} and b divides a and d divides c. Then \frac{a}{b} · \frac{c}{d} = \frac{a·c}{b·d}.

(15) For all elements a, b, c of the carrier of R such that a ≠ 0_{R} and a · b divides a · c holds b divides c.

(16) For every element a of the carrier of R such that a is associated to 0_{R} holds a = 0_{R}.

(17) For all elements a, b of the carrier of R such that a ≠ 0_{R} and a · b = a holds b = 1_{R}.

(18) Let a, b be elements of the carrier of R. Then a is associated to b if and only if there exists c such that c is unital and a · c = b.

(19) For all elements a, b, c of the carrier of R such that c ≠ 0_{R} and c · a is associated to c · b holds a is associated to b.

2. AmpleSets

Let R be an integral domain and let a be an element of the carrier of R. The functor Classesa yields a subset of the carrier of R and is defined as follows:

(Def. 5) For every element b of the carrier of R holds b ∈ Classesa iff b is asso-

ciated to a. Let R be an integral domain and let a be an element of the carrier of R.

Note that Classesa is non empty.

We now state the proposition

(20) For all elements a, b of the carrier of R such that Classesa∩Classesb ≠ ∅

holds Classesa = Classesb. Let R be an integral domain. The functor ClassesR yielding a family of

subsets of the carrier of R is defined by the condition (Def. 6). (Def. 6) Let A be a subset of the carrier of R. Then A ∈ ClassesR if and only if

there exists an element a of the carrier of R such that A = Classesa. Let R be an integral domain. One can check that ClassesR is non empty. We now state the proposition

(21) For every subset X of the carrier of R such that X ∈ ClassesR holds X

is non empty. Let R be an integral domain. A non empty subset of the carrier of R is said

to be an amp set of R if it satisfies the conditions (Def. 7). (Def. 7)(i) For every element a of the carrier of R holds there exists an element

of it which is associated to a, and (ii) for all elements x, y of it such that x ≠ y holds x is not associated to

y. Let R be an integral domain. A non empty subset of the carrier of R is called

an AmpleSet of R if: (Def. 8) It is an amp set of R and 1_{R} ∈ it.

In the sequel A_{1} denotes an AmpleSet of R. The following propositions are true:

(22) Let A_{1} be an AmpleSet of R. Then (i) 1_{R} ∈ A_{1}, (ii) for every element a of the carrier of R holds there exists an element of

A_{1} which is associated to a, and (iii) for all elements x, y of A_{1} such that x ≠ y holds x is not associated to

y.

(23) For all elements x, y of A_{1} such that x is associated to y holds x = y.

(24) For every AmpleSet A_{1} of R holds 0_{R} is an element of A_{1}.

Let R be an integral domain, let A_{1} be an AmpleSet of R, and let x be an element of the carrier of R. The functor NF(x, A_{1}) yields an element of the carrier of R and is defined as follows:

(Def. 9) NF(x, A_{1}) ∈ A_{1} and NF(x, A_{1}) is associated to x.

The following propositions are true:

(25) For every AmpleSet A_{1} of R holds NF(0_{R}, A_{1}) = 0_{R} and NF(1_{R}, A_{1}) = 1_{R}.

(26) For every AmpleSet A_{1} of R and for every element a of the carrier of R

holds a ∈ A_{1} iff a = NF(a, A_{1}). Let R be an integral domain and let A_{1} be an AmpleSet of R. We say that

A_{1} is multiplicative if and only if: (Def. 10) For all elements x, y of A_{1} holds x · y ∈ A_{1}.

The following proposition is true

(27) Let A_{1} be an AmpleSet of R. Suppose A_{1} is multiplicative. Let x, y be elements of A_{1}. If y divides x and y ≠ 0_{R}, then \frac{x}{y} ∈ A_{1}.

3. GCD-Domains

Let R be an integral domain. We say that R is gcd-like if and only if the condition (Def. 11) is satisfied.

(Def. 11) Let x, y be elements of the carrier of R. Then there exists an element z

of the carrier of R such that

(i) z divides x, (ii) z divides y, and (iii) for every element z_{1} of the carrier of R such that z_{1} divides x and z_{1}

divides y holds z_{1} divides z. Let us note that there exists an integral domain which is gcd-like. A gcdDomain is a gcd-like integral domain. Let R be a gcdDomain, let A_{1} be an AmpleSet of R, and let x, y be elements

of the carrier of R. The functor gcd_{A_{1}}(x, y) yielding an element of the carrier of R is defined by the conditions (Def. 12).

(Def. 12)(i) gcd_{A_{1}}(x, y) ∈ A_{1}, (ii) gcd_{A_{1}}(x, y) divides x, (iii) gcd_{A_{1}}(x, y) divides y, and (iv) for every element z of the carrier of R such that z divides x and z

divides y holds z divides gcd_{A_{1}}(x, y). In the sequel R is a gcdDomain. The following propositions are true:

(28) Let A_{1} be an AmpleSet of R and a, b be elements of the carrier of R. Then gcd_{A_{1}}(a, b) divides a and gcd_{A_{1}}(a, b) divides b.

(29) Let A_{1} be an AmpleSet of R and a, b, c be elements of the carrier of R. If c divides gcd_{A_{1}}(a, b), then c divides a and c divides b.

(30) For every AmpleSet A_{1} of R and for all elements a, b of the carrier of R holds gcd_{A_{1}}(a, b) = gcd_{A_{1}}(b, a).

(31) For every AmpleSet A_{1} of R and for every element a of the carrier of R holds gcd_{A_{1}}(a, 0_{R}) = NF(a, A_{1}) and gcd_{A_{1}}(0_{R}, a) = NF(a, A_{1}).

(32) For every AmpleSet A_{1} of R holds gcd_{A_{1}}(0_{R}, 0_{R}) = 0_{R}.

(33) For every AmpleSet A_{1} of R and for every element a of the carrier of R holds gcd_{A_{1}}(a, 1_{R}) = 1_{R} and gcd_{A_{1}}(1_{R}, a) = 1_{R}.

(34) Let A_{1} be an AmpleSet of R and a, b be elements of the carrier of R. Then gcd_{A_{1}}(a, b) = 0_{R} if and only if a = 0_{R} and b = 0_{R}.

(35) Let A_{1} be an AmpleSet of R and a, b, c be elements of the carrier of R. Suppose b is associated to c. Then gcd_{A_{1}}(a, b) is associated to gcd_{A_{1}}(a, c) and gcd_{A_{1}}(b, a) is associated to gcd_{A_{1}}(c, a).

(36) For every AmpleSet A_{1} of R and for all elements a, b, c of the carrier of R holds gcd_{A_{1}}(gcd_{A_{1}}(a, b), c) = gcd_{A_{1}}(a, gcd_{A_{1}}(b, c)).

(37) For every AmpleSet A_{1} of R and for all elements a, b, c of the carrier of R holds gcd_{A_{1}}(a · c, b · c) is associated to c · (gcd_{A_{1}}(a, b)).

(38) For every AmpleSet A_{1} of R and for all elements a, b, c of the carrier of R such that gcd_{A_{1}}(a, b) = 1_{R} holds gcd_{A_{1}}(a, b · c) = gcd_{A_{1}}(a, c).

(39) Let A_{1} be an AmpleSet of R and a, b, c be elements of the carrier of R. If c = gcd_{A_{1}}(a, b) and c ≠ 0_{R}, then gcd_{A_{1}}(\frac{a}{c}, \frac{b}{c}) = 1_{R}.

(40) For every AmpleSet A_{1} of R and for all elements a, b, c of the carrier of R holds gcd_{A_{1}}(a + b · c, c) = gcd_{A_{1}}(a, c).

4. The Theorems of Brown and Henrici

The following propositions are true:

(41) Let A_{1} be an AmpleSet of R and r_{1}, r_{2}, s_{1}, s_{2} be elements of the carrier of R. Suppose gcd_{A_{1}}(r_{1}, r_{2}) = 1_{R} and gcd_{A_{1}}(s_{1}, s_{2}) = 1_{R} and r_{2} ≠ 0_{R} and s_{2} ≠ 0_{R}. Then gcd_{A_{1}}(r_{1} · \frac{s_{2}}{gcd_{A_{1}}(r_{2},s_{2})} + s_{1} · \frac{r_{2}}{gcd_{A_{1}}(r_{2},s_{2})}, r_{2} · \frac{s_{2}}{gcd_{A_{1}}(r_{2},s_{2})}) = gcd_{A_{1}}(r_{1} · \frac{s_{2}}{gcd_{A_{1}}(r_{2},s_{2})} + s_{1} · \frac{r_{2}}{gcd_{A_{1}}(r_{2},s_{2})}, gcd_{A_{1}}(r_{2}, s_{2})).

(42) Let A_{1} be an AmpleSet of R and r_{1}, r_{2}, s_{1}, s_{2} be elements of the carrier of R. Suppose gcd_{A_{1}}(r_{1}, r_{2}) = 1_{R} and gcd_{A_{1}}(s_{1}, s_{2}) = 1_{R} and r_{2} ≠ 0_{R} and s_{2} ≠ 0_{R}. Then gcd_{A_{1}}(\frac{r_{1}}{gcd_{A_{1}}(r_{1},s_{2})} · \frac{s_{1}}{gcd_{A_{1}}(s_{1},r_{2})}, \frac{r_{2}}{gcd_{A_{1}}(s_{1},r_{2})} · \frac{s_{2}}{gcd_{A_{1}}(r_{1},s_{2})}) = 1_{R}.

5. Correctness of the Algorithms

Let R be a gcdDomain, let A_{1} be an AmpleSet of R, and let x, y be elements of the carrier of R. We say that x, y are canonical wrt A_{1} if and only if:

(Def. 13) gcd_{A_{1}}(x, y) = 1_{R}.

Next we state the proposition

(43) Let A_{1}, A′_{1} be AmpleSet of R and x, y be elements of the carrier of R.

Then x, y are canonical wrt A_{1} if and only if x, y are canonical wrt A′_{1}. Let R be a gcdDomain and let x, y be elements of the carrier of R. We say

that x canonical y if and only if: (Def. 14) There exists an AmpleSet A_{1} of R such that gcd_{A_{1}}(x, y) = 1_{R}.

Let us observe that the predicate x canonical y is symmetric.

Next we state the proposition

(44) Let A_{1} be an AmpleSet of R and x, y be elements of the carrier of R. If

x canonical y, then gcd_{A_{1}}(x, y) = 1_{R}. Let R be a gcdDomain, let A_{1} be an AmpleSet of R, and let x, y be elements

of the carrier of R. We say that x, y are normalized wrt A_{1} if and only if: (Def. 15) gcd_{A_{1}}(x, y) = 1_{R} and y ∈ A_{1} and y ≠ 0_{R}.

Let R be a gcdDomain, let A_{1} be an AmpleSet of R, and let r_{1}, r_{2}, s_{1}, s_{2} be elements of the carrier of R. Let us assume that r_{1} canonical r_{2} and s_{1} canonical s_{2} and r_{2} = NF(r_{2}, A_{1}) and s_{2} = NF(s_{2}, A_{1}). The functor add1_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) yielding an element of the carrier of R is defined as follows:

(Def. 16) add1_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) = \{ \begin{matrix}s_{1}, if r_{1} = 0_{R}, \\ r_{1}, if s_{1} = 0_{R}, \\ r_{1} · s_{2} + r_{2} · s_{1}, if gcd_{A_{1}}(r_{2}, s_{2}) = 1_{R}, \\ 0_{R}, if r_{1} · \frac{s_{2}}{gcd_{A_{1}}(r_{2},s_{2})} + s_{1} · \frac{r_{2}}{gcd_{A_{1}}(r_{2},s_{2})} = 0_{R}, \\ \frac{r_{1}·_{\frac{s_{2}}{gcd _{A_{1}} (r_{2},s_{2})}} +s_{1}·_{\frac{r_{2}}{gcd _{A_{1}} (r_{2},s_{2})}}}{gcd_{A_{1}}(r_{1}·_{\frac{s_{2}}{gcd _{A_{1}} (r_{2},s_{2})}} +s_{1}·_{\frac{r_{2}}{gcd _{A_{1}} (r_{2},s_{2})}} ,gcd_{A_{1}}(r_{2},s_{2}))}, \\ otherwise. \end{matrix}

Let R be a gcdDomain, let A_{1} be an AmpleSet of R, and let r_{1}, r_{2}, s_{1}, s_{2} be elements of the carrier of R. Let us assume that r_{1} canonical r_{2} and s_{1} canonical s_{2} and r_{2} = NF(r_{2}, A_{1}) and s_{2} = NF(s_{2}, A_{1}). The functor add2_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) yields an element of the carrier of R and is defined by:

(Def. 17) add2_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) = \{ \begin{matrix}s_{2}, if r_{1} = 0_{R}, \\ r_{2}, if s_{1} = 0_{R}, \\ r_{2} · s_{2}, if gcd_{A_{1}}(r_{2}, s_{2}) = 1_{R}, \\ 1_{R}, if r_{1} · \frac{s_{2}}{gcd_{A_{1}}(r_{2},s_{2})} + s_{1} · \frac{r_{2}}{gcd_{A_{1}}(r_{2},s_{2})} = 0_{R}, \\ \frac{r_{2}·_{\frac{s_{2}}{gcd _{A_{1}} (r_{2},s_{2})}}}{gcd_{A_{1}}(r_{1}·_{\frac{s_{2}}{gcd _{A_{1}} (r_{2},s_{2})}} +s_{1}·_{\frac{r_{2}}{gcd _{A_{1}} (r_{2},s_{2})}} ,gcd_{A_{1}}(r_{2},s_{2}))}, \\ otherwise. \end{matrix}

We now state two propositions:

(45) Let A_{1} be an AmpleSet of R and r_{1}, r_{2}, s_{1}, s_{2} be elements of the carrier of R. Suppose A_{1} is multiplicative and r_{1}, r_{2} are normalized wrt A_{1} and s_{1}, s_{2} are normalized wrt A_{1}. Then add1_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}), add2_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) are normalized wrt A_{1}.

(46) Let A_{1} be an AmpleSet of R and r_{1}, r_{2}, s_{1}, s_{2} be elements of the carrier of R. Suppose A_{1} is multiplicative and r_{1}, r_{2} are normalized wrt A_{1} and s_{1}, s_{2} are normalized wrt A_{1}. Then add1_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) · (r_{2} · s_{2}) = add2_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) · (r_{1} · s_{2} + s_{1} · r_{2}).

Let R be a gcdDomain, let A_{1} be an AmpleSet of R, and let r_{1}, r_{2}, s_{1}, s_{2} be elements of the carrier of R. The functor mult1_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) yields an element of the carrier of R and is defined as follows:

(Def. 18) mult1_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) = \{ \begin{matrix}0_{R}, if r_{1} = 0_{R} or s_{1} = 0_{R}, \\ r_{1} · s_{1}, if r_{2} = 1_{R} and s_{2} = 1_{R}, \\ \frac{r_{1}·s_{1}}{gcd_{A_{1}}(r_{1},s_{2})}, if s_{2} ≠ 0_{R} and r_{2} = 1_{R}, \\ \frac{r_{1}·s_{1}}{gcd_{A_{1}}(s_{1},r_{2})}, if r_{2} ≠ 0_{R} and s_{2} = 1_{R}, \\ \frac{r_{1}}{gcd_{A_{1}}(r_{1},s_{2})} · \frac{s_{1}}{gcd_{A_{1}}(s_{1},r_{2})}, otherwise. \end{matrix}

Let R be a gcdDomain, let A_{1} be an AmpleSet of R, and let r_{1}, r_{2}, s_{1}, s_{2} be elements of the carrier of R. Let us assume that r_{1} canonical r_{2} and s_{1} canonical s_{2} and r_{2} = NF(r_{2}, A_{1}) and s_{2} = NF(s_{2}, A_{1}). The functor mult2_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) yields an element of the carrier of R and is defined as follows:

(Def. 19) mult2_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) = \{ \begin{matrix}1_{R}, if r_{1} = 0_{R} or s_{1} = 0_{R}, \\ 1_{R}, if r_{2} = 1_{R} and s_{2} = 1_{R}, \\ \frac{s_{2}}{gcd_{A_{1}}(r_{1},s_{2})}, if s_{2} ≠ 0_{R} and r_{2} = 1_{R}, \\ \frac{r_{2}}{gcd_{A_{1}}(s_{1},r_{2})}, if r_{2} ≠ 0_{R} and s_{2} = 1_{R}, \\ \frac{r_{2}}{gcd_{A_{1}}(s_{1},r_{2})} · \frac{s_{2}}{gcd_{A_{1}}(r_{1},s_{2})}, otherwise. \end{matrix}

The following two propositions are true:

(47) Let A_{1} be an AmpleSet of R and r_{1}, r_{2}, s_{1}, s_{2} be elements of the carrier of R. Suppose A_{1} is multiplicative and r_{1}, r_{2} are normalized wrt A_{1} and s_{1}, s_{2} are normalized wrt A_{1}. Then mult1_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}), mult2_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) are normalized wrt A_{1}.

(48) Let A_{1} be an AmpleSet of R and r_{1}, r_{2}, s_{1}, s_{2} be elements of the carrier of R. Suppose A_{1} is multiplicative and r_{1}, r_{2} are normalized wrt A_{1} and s_{1}, s_{2} are normalized wrt A_{1}. Then mult1_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) · (r_{2} · s_{2}) = mult2_{A_{1}}(r_{1}, r_{2}, s_{1}, s_{2}) · (r_{1} · s_{1}).

References

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

[2] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3–11, 1991.

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

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

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

[6] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

Birkhoff Theorem for Many Sorted Algebras

Artur Korniłowicz Warsaw University Białystok

Summary. In this article Birkhoff Variety Theorem for many sorted algebras is proved. A class of algebras is represented by predicate P. Notation P[A], where A is an algebra, means that A is in class P. All algebras in our class are many sorted over many sorted signature S. The properties of varieties:

• a class P of algebras is abstract

• a class P of algebras is closed under subalgebras

• a class P of algebras is closed under congruences

• a class P of algebras is closed under products are published in this paper as:

• for all non-empty algebras A, B over S such that A and B are isomorphic and P[A] holds P[B]

• for every non-empty algebra A over S and for strict non-empty subalgebra B of A such that P[A] holds P[B]

• for every non-empty algebra A over S and for every congruence R of A such that P[A] holds P[A/R]

• Let I be a set and F be an algebra family of I over A. Suppose that for every set i such that i ∈ I there exists an algebra A over A such that A = F (i) and P[A]. ThenP[∏ F].

This paper is formalization of parts of [29].

MML Identifier: BIRKHOFF.

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

Let S be a non empty non void many sorted signature, let X be a non-empty many sorted set indexed by the carrier of S, let A be a non-empty algebra over S, and let F be a many sorted function from X into the sorts of A. The functor F^{#} yielding a many sorted function from Free(X) into A is defined by:

(Def. 1) F^{#} is a homomorphism of Free(X) into A and F^{#} ↾ FreeGenerator(X) =

F ∘ Reverse(X). We now state the proposition

(1) Let S be a non empty non void many sorted signature, A be a non-empty algebra over S, X be a non-empty many sorted set indexed by the carrier of S, and F be a many sorted function from X into the sorts of A. Then rng_{κ} F (κ) ⊆ rng_{κ} F^{#}(κ).

In this article we present several logical schemes. The scheme ExFreeAlg 1 concerns a non empty non void many sorted signature A, a non-empty algebra B over A, and a unary predicate P, and states that:

There exists a strict non-empty algebra A over A and there exists a many sorted function F from B into A such that

(i) P[A], (ii) F is an epimorphism of B onto A, and (iii) for every non-empty algebra B over A and for every many sorted function G from B into B such that G is a homomorphism of B into B and P[B] there exists a many sorted function H from A into B such that H is a homomorphism of A into B and H ∘ F = G and for every many sorted function K from A into B such that K ∘ F = G holds H = K

provided the following conditions are met:

• For all non-empty algebras A, B over A such that A and B are isomorphic and P[A] holds P[B],

• For every non-empty algebra A over A and for every strict nonempty subalgebra B of A such that P[A] holds P[B], and

• Let I be a set and F be an algebra family of I over A. Suppose that for every set i such that i ∈ I there exists an algebra A over A such that A = F (i) and P[A]. Then P[∏ F].

The scheme ExFreeAlg 2 concerns a non empty non void many sorted signature A, a non-empty many sorted set B indexed by the carrier of A, and a unary predicate P, and states that:

There exists a strict non-empty algebra A over A and there exists a many sorted function F from B into the sorts of A such that

(i) P[A], and (ii) for every non-empty algebra B over A and for every many sorted function G from B into the sorts of B such that P[B] there exists a many sorted function H from A into B such that H is a homomorphism of A into B and H ∘ F = G and for every many sorted function K from A into B such that K is a homomorphism of A into B and K ∘ F = G holds H = K

provided the following requirements are met:

• For all non-empty algebras A, B over A such that A and B are isomorphic and P[A] holds P[B],

• For every non-empty algebra A over A and for every strict nonempty subalgebra B of A such that P[A] holds P[B], and

• Let I be a set and F be an algebra family of I over A. Suppose that for every set i such that i ∈ I there exists an algebra A over A such that A = F (i) and P[A]. Then P[∏ F].

The scheme Ex hash concerns a non empty non void many sorted signature A, non-empty algebras B, C over A, a many sorted function D from the carrier of A ⟼→ ℕ into the sorts of B, a many sorted function E from the carrier of A ⟼→ ℕ into the sorts of C, and a unary predicate P, and states that:

There exists a many sorted function H from B into C such that H is a homomorphism of B into C and E^{#} = H ∘ D^{#}

provided the parameters have the following properties:

• P[C], and

• Let C be a non-empty algebra over A and G be a many sorted function from (the carrier of A) ⟼→ ℕ into the sorts of C. Suppose P[C]. Then there exists a many sorted function h from B into C such that h is a homomorphism of B into C and G = h ∘ D.

The scheme EqTerms concerns a non empty non void many sorted signature A, a non-empty algebra B over A, a many sorted function C from the carrier of A ⟼→ ℕ into the sorts of B, a sort symbol D of A, elements E, F of the sorts of T_{A}(ℕ)(D), and a unary predicate P, and states that:

For every non-empty algebra B over A such that P[B] holds B ⊧ ⟨⟨E, F⟩⟩

provided the parameters have the following properties:

• C^{#}(D)(E) = C^{#}(D)(F), and

• Let C be a non-empty algebra over A and G be a many sorted function from (the carrier of A) ⟼→ ℕ into the sorts of C. Suppose P[C]. Then there exists a many sorted function h from B into C such that h is a homomorphism of B into C and G = h ∘ C.

The scheme FreeIsGen deals with a non empty non void many sorted signature A, a non-empty many sorted set B indexed by the carrier of A, a strict non-empty algebra C over A, a many sorted function D from B into the sorts of C, and a unary predicate P, and states that:

D^{∘} B is a non-empty generator set of C provided the parameters satisfy the following conditions:

• Let C be a non-empty algebra over A and G be a many sorted function from B into the sorts of C. Suppose P[C]. Then there exists a many sorted function H from C into C such that

(i) H is a homomorphism of C into C, (ii) H ∘ D = G, and (iii) for every many sorted function K from C into C such that K is a homomorphism of C into C and K ∘ D = G holds H = K,

• P[C], and

• For every non-empty algebra A over A and for every strict nonempty subalgebra B of A such that P[A] holds P[B].

The scheme Hash is onto deals with a non empty non void many sorted signature A, a strict non-empty algebra B over A, a many sorted function C from the carrier of A ⟼→ ℕ into the sorts of B, and a unary predicate P, and states that:

C^{#} is an epimorphism of Free((the carrier of A) ⟼→ ℕ) onto B provided the following conditions are satisfied:

• Let C be a non-empty algebra over A and G be a many sorted function from (the carrier of A) ⟼→ ℕ into the sorts of C. Suppose P[C]. Then there exists a many sorted function H from B into C such that

(i) H is a homomorphism of B into C, (ii) H ∘ C = G, and (iii) for every many sorted function K from B into C such that K is a homomorphism of B into C and K ∘ C = G holds H = K,

• P[B], and

• For every non-empty algebra A over A and for every strict nonempty subalgebra B of A such that P[A] holds P[B].

The scheme FinGenAlgInVar concerns a non empty non void many sorted signature A, a strict finitely-generated non-empty algebra B over A, a nonempty algebra C over A, a many sorted function D from the carrier of A ⟼→ ℕ into the sorts of C, and two unary predicates P, Q, and states that:

P[B] provided the parameters satisfy the following conditions:

• Q[B],

• P[C],

• Let C be a non-empty algebra over A and G be a many sorted function from (the carrier of A) ⟼→ ℕ into the sorts of C. Suppose Q[C]. Then there exists a many sorted function h from C into C such that h is a homomorphism of C into C and G = h ∘ D,

• For all non-empty algebras A, B over A such that A and B are isomorphic and P[A] holds P[B], and

• For every non-empty algebra A over A and for every congruence R of A such that P[A] holds P[A/R].

The scheme QuotEpi concerns a non empty non void many sorted signature A, non-empty algebras B, C over A, and a unary predicate P, and states that:

P[C] provided the following conditions are satisfied:

• There exists a many sorted function from B into C which is an epimorphism of B onto C,

• P[B],

• For all non-empty algebras A, B over A such that A and B are isomorphic and P[A] holds P[B], and

• For every non-empty algebra A over A and for every congruence R of A such that P[A] holds P[A/R].

The scheme AllFinGen deals with a non empty non void many sorted signature A, a non-empty algebra B over A, and a unary predicate P, and states that:

P[B] provided the parameters satisfy the following conditions:

• For every strict non-empty finitely-generated subalgebra B of B holds P[B],

• For all non-empty algebras A, B over A such that A and B are isomorphic and P[A] holds P[B],

• For every non-empty algebra A over A and for every strict nonempty subalgebra B of A such that P[A] holds P[B],

• For every non-empty algebra A over A and for every congruence R of A such that P[A] holds P[A/R], and

• Let I be a set and F be an algebra family of I over A. Suppose that for every set i such that i ∈ I there exists an algebra A over A such that A = F (i) and P[A]. Then P[∏ F].

The scheme FreeInModIsInVar 1 deals with a non empty non void many sorted signature A, a non-empty algebra B over A, and two unary predicates P, Q, and states that:

Q[B] provided the following requirements are met:

• Let A be a non-empty algebra over A. Then Q[A] if and only if for every sort symbol s of A and for every element e of (the equations of A)(s) such that for every non-empty algebra B over A such that P[B] holds B ⊧ e holds A ⊧ e, and

• P[B]. The scheme FreeInModIsInVar deals with a non empty non void many sorted

signature A, a strict non-empty algebra B over A, a many sorted function C from the carrier of A ⟼→ ℕ into the sorts of B, and two unary predicates P, Q, and states that:

P[B] provided the parameters meet the following conditions:

• Let A be a non-empty algebra over A. Then Q[A] if and only if for every sort symbol s of A and for every element e of (the equations of A)(s) such that for every non-empty algebra B over A such that P[B] holds B ⊧ e holds A ⊧ e,

• Let C be a non-empty algebra over A and G be a many sorted function from (the carrier of A) ⟼→ ℕ into the sorts of C. Suppose Q[C]. Then there exists a many sorted function H from B into C such that

(i) H is a homomorphism of B into C, (ii) H ∘ C = G, and (iii) for every many sorted function K from B into C such that K is a homomorphism of B into C and K ∘ C = G holds H = K,

• Q[B],

• For all non-empty algebras A, B over A such that A and B are isomorphic and P[A] holds P[B],

• For every non-empty algebra A over A and for every strict nonempty subalgebra B of A such that P[A] holds P[B], and

• Let I be a set and F be an algebra family of I over A. Suppose that for every set i such that i ∈ I there exists an algebra A over A such that A = F (i) and P[A]. Then P[∏ F].

The scheme Birkhoff deals with a non empty non void many sorted signature A and a unary predicate P, and states that:

There exists a set E of equations of A such that for every nonempty algebra A over A holds P[A] iff A ⊧ E

provided the parameters meet the following conditions:

• For all non-empty algebras A, B over A such that A and B are isomorphic and P[A] holds P[B],

• For every non-empty algebra A over A and for every strict nonempty subalgebra B of A such that P[A] holds P[B],

• For every non-empty algebra A over A and for every congruence R of A such that P[A] holds P[A/R], and

• Let I be a set and F be an algebra family of I over A. Suppose that for every set i such that i ∈ I there exists an algebra A over A such that A = F (i) and P[A]. Then P[∏ F].

References

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

[2] Ewa Burakowska. Subalgebras of many sorted algebra. Lattice of subalgebras. Formalized Mathematics, 5(1):47–54, 1996.

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

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

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

[6] Mariusz Giero. More on products of many sorted algebras. Formalized Mathematics, 5(4):621–626, 1996.

birkhoff theorem for many sorted algebras 395

[7] Artur Korniłowicz. Certain facts about families of subsets of many sorted sets. Formalized Mathematics, 5(3):451–456, 1996.

[8] Artur Korniłowicz. Extensions of mappings on generator set. Formalized Mathematics, 5(2):269–272, 1996.

[9] Artur Korniłowicz. On the closure operator and the closure system of many sorted sets. Formalized Mathematics, 5(4):543–551, 1996.

[10] Artur Korniłowicz. On the group of automorphisms of universal algebra & many sorted algebra. Formalized Mathematics, 5(2):221–226, 1996.

[11] Artur Korniłowicz. Some basic properties of many sorted sets. Formalized Mathematics, 5(3):395–399, 1996.

[12] Artur Korniłowicz. Equations in many sorted algebras. Formalized Mathematics, 6(3):363–369, 1997.

[13] Małgorzata Korolkiewicz. Homomorphisms of many sorted algebras. Formalized Mathematics, 5(1):61–65, 1996.

[14] Małgorzata Korolkiewicz. Many sorted quotient algebra. Formalized Mathematics, 5(1):79–84, 1996.

[15] Beata Madras. Product of family of universal algebras. Formalized Mathematics, 4(1):103– 108, 1993.

[16] Beata Madras. Products of many sorted algebras. Formalized Mathematics, 5(1):55–60, 1996.

[17] Robert Milewski. Lattice of congruences in many sorted algebra. Formalized Mathematics, 5(4):479–483, 1996.

[18] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, II. Formalized Mathematics, 5(2):215–220, 1996.

[19] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Formalized Mathematics, 5(2):167–172, 1996.

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

[21] Beata Perkowska. Free many sorted universal algebra. Formalized Mathematics, 5(1):67– 74, 1996.

[22] Konrad Raczkowski and Paweł Sadowski. Equivalence relations and classes of abstraction. Formalized Mathematics, 1(3):441–444, 1990.

[23] Alexander Yu. Shibakov and Andrzej Trybulec. The Cantor set. Formalized Mathematics, 5(2):233–236, 1996.

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

[25] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

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

[27] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37–42, 1996.

[28] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

[29] Wolfgang Wechler. Universal Algebra for Computer Scientists, volume 25 of EATCS Monographs on TCS. Springer–Verlag, 1992.

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

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

396 artur korniłowicz

Algebraic Operation on Subsets of Many Sorted Sets

Agnieszka Julia Marasik Warsaw University Białystok

MML Identifier: CLOSURE3.

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

1. Preliminaries

Let S be a non empty 1-sorted structure. One can verify that the 1-sorted structure of S is non empty.

We now state three propositions:

(1) For every non empty set I and for all many sorted sets M, N indexed by I holds M+·N = N.

(2) Let I be a set, M, N be many sorted sets indexed by I, and F be a family of many sorted subsets indexed by M. If N ∈ F, then ⋂ |:F:| ⊆ N.

(3) Let S be a non void non empty many sorted signature, M_{1} be a strict non-empty algebra over S, and F be a family of many sorted subsets indexed by the sorts of M_{1}. Suppose F ⊆ SubSorts(M_{1}). Let B be a subset of M_{1}. If B = ⋂ |:F:|, then B is operations closed.

2. Relationships between Subsets Families

Let I be a set, let M be a many sorted set indexed by I, let B be a family of many sorted subsets indexed by M, and let A be a family of many sorted subsets indexed by M. We say that A is finer than B if and only if:

(Def. 1) For every set a such that a ∈ A there exists a set b such that b ∈ B and

a ⊆ b. Let us observe that the predicate A is finer than B is reflexive. We say that B is coarser than A if and only if:

(Def. 2) For every set b such that b ∈ B there exists a set a such that a ∈ A and

a ⊆ b. Let us notice that the predicate B is coarser than A is reflexive.

We now state two propositions:

(4) Let I be a set, M be a many sorted set indexed by I, and A, B, C be families of many sorted subsets indexed by M. If A is finer than B and B is finer than C, then A is finer than C.

(5) Let I be a set, M be a many sorted set indexed by I, and A, B, C be families of many sorted subsets indexed by M. If A is coarser than B and B is coarser than C, then A is coarser than C.

Let I be a non empty set and let M be a many sorted set indexed by I. The functor supp(M) yielding a set is defined by:

(Def. 3) supp(M) = {x, x ranges over elements of I: M(x) ≠ ∅}.

We now state four propositions:

(6) For every non empty set I and for every non-empty many sorted set M indexed by I holds M = ∅_{I}+·M↾ supp(M).

(7) Let I be a non empty set and M_{2}, M_{3} be non-empty many sorted sets indexed by I. If supp(M_{2}) = supp(M_{3}) and M_{2}↾ supp(M_{2}) = M_{3}↾ supp(M_{3}), then M_{2} = M_{3}.

(8) Let I be a non empty set, M be a many sorted set indexed by I, and x be an element of I. If x ∉ supp(M), then M(x) = ∅.

(9) Let I be a non empty set, M be a many sorted set indexed by I, x be an element of Bool(M), i be an element of I, and y be a set. Suppose y ∈ x(i). Then there exists an element a of Bool(M) such that y ∈ a(i) and a is locally-finite and supp(a) is finite and a ⊆ x.

Let I be a set, let M be a many sorted set indexed by I, and let A be a family of many sorted subsets indexed by M. The functor MSUnion(A) yielding a many sorted subset indexed by M is defined by:

(Def. 4) For every set i such that i ∈ I holds (MSUnion(A))(i) = ⋃{f(i), f ranges over elements of Bool(M): f ∈ A}.

Let I be a set, let M be a many sorted set indexed by I, and let B be a non empty family of many sorted subsets indexed by M. We see that the element of B is a many sorted set indexed by I.

Let I be a set, let M be a many sorted set indexed by I, and let A be an empty family of many sorted subsets indexed by M. One can check that MSUnion(A) is empty yielding.

We now state the proposition

(10) Let I be a set, M be a many sorted set indexed by I, and A be a family

of many sorted subsets indexed by M. Then MSUnion(A) = ⋃ |:A:|. Let I be a set, let M be a many sorted set indexed by I, and let A, B be

families of many sorted subsets indexed by M. Then A ∪ B is a family of many sorted subsets indexed by M.

The following propositions are true:

(11) Let I be a set, M be a many sorted set indexed by I, and A, B be families of many sorted subsets indexed by M. Then MSUnion(A ∪ B) = MSUnion(A) ∪ MSUnion(B).

(12) Let I be a set, M be a many sorted set indexed by I, and A, B be families of many sorted subsets indexed by M. If A ⊆ B, then MSUnion(A) ⊆ MSUnion(B).

Let I be a set, let M be a many sorted set indexed by I, and let A, B be families of many sorted subsets indexed by M. Then A ∩ B is a family of many sorted subsets indexed by M.

One can prove the following propositions:

(13) Let I be a set, M be a many sorted set indexed by I, and A, B be families of many sorted subsets indexed by M. Then MSUnion(A ∩ B) ⊆ MSUnion(A) ∩ MSUnion(B).

(14) Let I be a set, M be a many sorted set indexed by I, and A_{1} be a set. Suppose that for every set x such that x ∈ A_{1} holds x is a family of many sorted subsets indexed by M. Let A, B be families of many sorted subsets indexed by M. Suppose B = {MSUnion(X), X ranges over families of many sorted subsets indexed by M: X ∈ A_{1}} and A = ⋃ A_{1}. Then MSUnion(B) = MSUnion(A).

(15) Let I be a non empty set, M, N be many sorted sets indexed by I, and A be a family of many sorted subsets indexed by M. If for every many sorted set x indexed by I holds x ⊆ N, then MSUnion(A) ⊆ N.

3. Algebraic Operation on Subsets of Many Sorted Sets

Let I be a non empty set, let M be a many sorted set indexed by I, and let S be a set operation in M. We say that S is algebraic if and only if the condition (Def. 5) is satisfied.

(Def. 5) Let x be an element of Bool(M). Suppose x = S(x). Then there exists a family A of many sorted subsets indexed by M such that A = {S(a), a ranges over elements of Bool(M): a is locally-finite ∧ supp(a) is finite ∧ a ⊆ x} and x = MSUnion(A).

Let I be a non empty set and let M be a many sorted set indexed by I. Note that there exists a set operation in M which is algebraic, reflexive, monotonic, and idempotent.

Let S be a non empty 1-sorted structure and let I_{1} be a closure system of S. We say that I_{1} is algebraic if and only if:

(Def. 6) ClOp(I_{1}) is algebraic.

Let S be a non void non empty many sorted signature and let M_{1} be a nonempty algebra over S. The functor SubAlgCl(M_{1}) yields a strict closure system structure over S and is defined by:

(Def. 7) The sorts of SubAlgCl(M_{1}) = the sorts of M_{1} and the family of

SubAlgCl(M_{1}) = SubSorts(M_{1}). One can prove the following proposition

(16) Let S be a non void non empty many sorted signature and M_{1} be a strict non-empty algebra over S. Then SubSorts(M_{1}) is an absolutelymultiplicative family of many sorted subsets indexed by the sorts of M_{1}.

Let S be a non void non empty many sorted signature and let M_{1} be a strict non-empty algebra over S. Note that SubAlgCl(M_{1}) is absolutely-multiplicative.

Let S be a non void non empty many sorted signature and let M_{1} be a strict non-empty algebra over S. Observe that SubAlgCl(M_{1}) is algebraic.

References

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

[2] Ewa Burakowska. Subalgebras of many sorted algebra. Lattice of subalgebras. Formalized Mathematics, 5(1):47–54, 1996.

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

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

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

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

[7] Artur Korniłowicz. Certain facts about families of subsets of many sorted sets. Formalized Mathematics, 5(3):451–456, 1996.

algebraic operation on subsets of many … 401

[8] Artur Korniłowicz. Definitions and basic properties of boolean & union of many sorted sets. Formalized Mathematics, 5(2):279–281, 1996.

[9] Artur Korniłowicz. On the closure operator and the closure system of many sorted sets. Formalized Mathematics, 5(4):543–551, 1996.

[10] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Formalized Mathematics, 5(2):167–172, 1996.

[11] Andrzej Nędzusiak. σ-fields and probability. Formalized Mathematics, 1(2):401–407, 1990.

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

[13] Alexander Yu. Shibakov and Andrzej Trybulec. The Cantor set. Formalized Mathematics, 5(2):233–236, 1996.

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

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

[16] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37–42, 1996.

[17] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

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

402 agnieszka julia marasik

Convergence and the Limit of Complex Sequences. Serieses

Yasunari Shidama Shinshu University Nagano Artur Korniłowicz Warsaw University Białystok

MML Identifier: COMSEQ 3.

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

1. Preliminaries

For simplicity, we adopt the following convention: r_{1}, r_{2}, r_{3} are sequences of real numbers, s_{1}, s_{2}, s_{3} are complex sequences, k, n, m are natural numbers, and p, r are elements of ℝ.

The following propositions are true:

(1) (n + 1) + 0i ≠ 0_{ℂ} and 0 + (n + 1)i ≠ 0_{ℂ}.

(2) If for every n holds r_{1}(n) = 0, then for every m holds (∑_{α=0}^{κ} |r_{1}|(α))_{κ∈ℕ}(m) = 0.

(3) If for every n holds r_{1}(n) = 0, then r_{1} is absolutely summable.

Let us note that there exists a sequence of real numbers which is absolutely summable.

One can check that every sequence of real numbers which is summable is also convergent.

One can verify that every sequence of real numbers which is absolutely summable is also summable.

One can check that there exists a sequence of real numbers which is absolutely summable.

Next we state several propositions:

(4) Suppose r_{1} is convergent. Let given p. Suppose 0 < p. Then there exists n such that for all natural numbers m, l such that n m and n l holds |r_{1}(m) − r_{1}(l)| < p.

(5) If for every n holds r_{1}(n) p, then for all natural numbers n, l holds (∑_{α=0}^{κ}(r_{1})(α))_{κ∈ℕ}(n + l) − (∑_{α=0}^{κ}(r_{1})(α))_{κ∈ℕ}(n) p · l.

(6) If for every n holds r_{1}(n) p, then for every n holds (∑_{α=0}^{κ}(r_{1})(α))_{κ∈ℕ}(n) p · (n + 1).

(7) If for every n such that n m holds r_{2}(n) p · r_{3}(n), then (∑_{α=0}^{κ}(r_{2})(α))_{κ∈ℕ}(m) p · (∑_{α=0}^{κ}(r_{3})(α))_{κ∈ℕ}(m).

(8) Suppose that for every n such that n m holds r_{2}(n) p · r_{3}(n). Let given n. Suppose n m. Let l be a natural number. If n + l m, then (∑_{α=0}^{κ}(r_{2})(α))_{κ∈ℕ}(n + l) − (∑_{α=0}^{κ}(r_{2})(α))_{κ∈ℕ}(n) p · ((∑_{α=0}^{κ}(r_{3})(α))_{κ∈ℕ}(n + l) − (∑_{α=0}^{κ}(r_{3})(α))_{κ∈ℕ}(n)).

(9) If for every n holds 0 r_{1}(n), then for all n, m such that n m holds |(∑_{α=0}^{κ}(r_{1})(α))_{κ∈ℕ}(m) − (∑_{α=0}^{κ}(r_{1})(α))_{κ∈ℕ}(n)| = (∑_{α=0}^{κ}(r_{1})(α))_{κ∈ℕ}(m) − (∑_{α=0}^{κ}(r_{1})(α))_{κ∈ℕ}(n) and for every n holds |(∑_{α=0}^{κ}(r_{1})(α))_{κ∈ℕ}(n)| = (∑_{α=0}^{κ}(r_{1})(α))_{κ∈ℕ}(n).

(10) If s_{2} is convergent and s_{3} is convergent and lim(s_{2} − s_{3}) = 0_{ℂ}, then lims_{2} = lims_{3}.

2. The Operations on Complex Sequences

In the sequel z denotes an element of ℂ and N_{1} denotes an increasing sequence of naturals.

Let z be an element of ℂ. The functor (z^{κ})_{κ∈ℕ} yielding a complex sequence is defined as follows:

(Def. 1) (z^{κ})_{κ∈ℕ}(0) = 1_{ℂ} and for every n holds (z^{κ})_{κ∈ℕ}(n + 1) = (z^{κ})_{κ∈ℕ}(n) · z.

Let z be an element of ℂ and let n be a natural number. The functor z_{ℕ}^{n} yielding an element of ℂ is defined by:

(Def. 2) z_{ℕ}^{n} = (z^{κ})_{κ∈ℕ}(n).

The following proposition is true

(11) z_{ℕ}^{0} = 1_{ℂ}.

Let c be a complex sequence. The functor ℜ(c) yields a sequence of real numbers and is defined as follows:

(Def. 3) For every n holds ℜ(c)(n) = ℜ(c(n)).

Let c be a complex sequence. The functor ℑ(c) yielding a sequence of real numbers is defined as follows:

(Def. 4) For every n holds ℑ(c)(n) = ℑ(c(n)).

We now state a number of propositions:

(12) |z| |ℜ(z)| + |ℑ(z)|.

(13) |ℜ(z)| |z| and |ℑ(z)| |z|.

(14) ℜ(s_{2}) = ℜ(s_{3}) and ℑ(s_{2}) = ℑ(s_{3}) iff s_{2} = s_{3}.

(15) ℜ(s_{2}) + ℜ(s_{3}) = ℜ(s_{2} + s_{3}) and ℑ(s_{2}) + ℑ(s_{3}) = ℑ(s_{2} + s_{3}).

(16) − ℜ(s_{1}) = ℜ(− s_{1}) and − ℑ(s_{1}) = ℑ(− s_{1}).

(17) r · ℜ(z) = ℜ((r + 0i) · z) and r · ℑ(z) = ℑ((r + 0i) · z).

(18) ℜ(s_{2}) − ℜ(s_{3}) = ℜ(s_{2} − s_{3}) and ℑ(s_{2}) − ℑ(s_{3}) = ℑ(s_{2} − s_{3}).

(19) r ℜ(s_{1}) = ℜ((r + 0i) s_{1}) and r ℑ(s_{1}) = ℑ((r + 0i) s_{1}).

(20) ℜ(z s_{1}) = ℜ(z) ℜ(s_{1})−ℑ(z) ℑ(s_{1}) and ℑ(z s_{1}) = ℜ(z) ℑ(s_{1})+ℑ(z) ℜ(s_{1}).

(21) ℜ(s_{2} s_{3}) = ℜ(s_{2}) ℜ(s_{3}) − ℑ(s_{2}) ℑ(s_{3}) and ℑ(s_{2} s_{3}) = ℜ(s_{2}) ℑ(s_{3}) +

ℑ(s_{2}) ℜ(s_{3}). Let s_{1} be a complex sequence and let N_{1} be an increasing sequence of natu-

rals. The functor s_{1} N_{1} yielding a complex sequence is defined by: (Def. 5) For every n holds (s_{1} N_{1})(n) = s_{1}(N_{1}(n)).

Next we state the proposition

(22) ℜ(s_{1} N_{1}) = ℜ(s_{1}) · N_{1} and ℑ(s_{1} N_{1}) = ℑ(s_{1}) · N_{1}.

Let s_{1} be a complex sequence and let k be a natural number. The functor s_{1} ↑ k yields a complex sequence and is defined by:

(Def. 6) For every n holds (s_{1} ↑ k)(n) = s_{1}(n + k).

The following proposition is true

(23) ℜ(s_{1}) ↑ k = ℜ(s_{1} ↑ k) and ℑ(s_{1}) ↑ k = ℑ(s_{1} ↑ k).

Let s_{1} be a complex sequence. The functor (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ} yields a complex sequence and is defined as follows:

(Def. 7) (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(0) = s_{1}(0) and for every n holds (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(n+

1) = (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(n) + s_{1}(n + 1). Let s_{1} be a complex sequence. The functor ∑ s_{1} yields an element of ℂ and

is defined as follows: (Def. 8) ∑ s_{1} = lim((∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}).

Next we state a number of propositions:

(24) If for every n holds s_{1}(n) = 0_{ℂ}, then for every m holds (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(m) = 0_{ℂ}.

(25) If for every n holds s_{1}(n) = 0_{ℂ}, then for every m holds (∑_{α=0}^{κ} |s_{1}|(α))_{κ∈ℕ}(m) = 0.

(26) (∑_{α=0}^{κ} ℜ(s_{1})(α))_{κ∈ℕ} = ℜ((∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}) and (∑_{α=0}^{κ} ℑ(s_{1})(α))_{κ∈ℕ} = ℑ((∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}).

(27) (∑_{α=0}^{κ}(s_{2})(α))_{κ∈ℕ} + (∑_{α=0}^{κ}(s_{3})(α))_{κ∈ℕ} = (∑_{α=0}^{κ}(s_{2} + s_{3})(α))_{κ∈ℕ}.

(28) (∑_{α=0}^{κ}(s_{2})(α))_{κ∈ℕ} − (∑_{α=0}^{κ}(s_{3})(α))_{κ∈ℕ} = (∑_{α=0}^{κ}(s_{2} − s_{3})(α))_{κ∈ℕ}.

(29) (∑_{α=0}^{κ}(z s_{1})(α))_{κ∈ℕ} = z (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}.

(30) |(∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(k)| (∑_{α=0}^{κ} |s_{1}|(α))_{κ∈ℕ}(k).

(31) |(∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(m)−(∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(n)| |(∑_{α=0}^{κ} |s_{1}|(α))_{κ∈ℕ}(m) −(∑_{α=0}^{κ} |s_{1}|(α))_{κ∈ℕ}(n)|.

(32) (∑_{α=0}^{κ} ℜ(s_{1})(α))_{κ∈ℕ} ↑ k = ℜ((∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ} ↑ k) and (∑_{α=0}^{κ} ℑ(s_{1})(α))_{κ∈ℕ} ↑ k = ℑ((∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ} ↑ k).

(33) If for every n holds s_{2}(n) = s_{1}(0), then (∑_{α=0}^{κ}(s_{1} ↑ 1)(α))_{κ∈ℕ} = (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ} ↑ 1 − s_{2}.

(34) (∑_{α=0}^{κ} |s_{1}|(α))_{κ∈ℕ} is non-decreasing.

Let s_{1} be a complex sequence. Note that (∑_{α=0}^{κ} |s_{1}|(α))_{κ∈ℕ} is non-decreasing. Next we state three propositions:

(35) If for every n such that n m holds s_{2}(n) = s_{3}(n), then (∑_{α=0}^{κ}(s_{2})(α))_{κ∈ℕ}(m) = (∑_{α=0}^{κ}(s_{3})(α))_{κ∈ℕ}(m).

(36) If 1_{ℂ} ≠ z, then for every n holds (∑_{α=0}^{κ}((z^{κ})_{κ∈ℕ})(α))_{κ∈ℕ}(n) = \frac{1_{ℂ}−z_{ℕ}^{n+1}}{1_{ℂ}−z} .

(37) If z ≠ 1_{ℂ} and for every n holds s_{1}(n + 1) = z · s_{1}(n), then for every n holds (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(n) = s_{1}(0) · \frac{1_{ℂ}−z_{ℕ}^{n+1}}{1_{ℂ}−z} .

3. Convergence of Complex Sequences

Next we state four propositions:

(38) Let a, b be sequences of real numbers and c be a complex sequence. Suppose that for every n holds ℜ(c(n)) = a(n) and ℑ(c(n)) = b(n). Then a is convergent and b is convergent if and only if c is convergent.

(39) Let a, b be convergent sequences of real numbers and c be a complex sequence. Suppose that for every n holds ℜ(c(n)) = a(n) and ℑ(c(n)) = b(n). Then c is convergent and limc = lima + limbi.

(40) Let a, b be sequences of real numbers and c be a convergent complex sequence. Suppose that for every n holds ℜ(c(n)) = a(n) and ℑ(c(n)) = b(n). Then a is convergent and b is convergent and lima = ℜ(limc) and limb = ℑ(limc).

(41) For every convergent complex sequence c holds ℜ(c) is convergent and

ℑ(c) is convergent and limℜ(c) = ℜ(limc) and limℑ(c) = ℑ(limc). Let c be a convergent complex sequence. Observe that ℜ(c) is convergent

and ℑ(c) is convergent.

The following propositions are true:

(42) Let c be a complex sequence. Suppose ℜ(c) is convergent and ℑ(c) is convergent. Then c is convergent and ℜ(limc) = limℜ(c) and ℑ(limc) = limℑ(c).

(43) If 0 < |z| and |z| < 1 and s_{1}(0) = z and for every n holds s_{1}(n + 1) = s_{1}(n) · z, then s_{1} is convergent and lims_{1} = 0_{ℂ}.

(44) If |z| < 1 and for every n holds s_{1}(n) = z_{ℕ}^{n+1}, then s_{1} is convergent and lims_{1} = 0_{ℂ}.

(45) If r > 0 and there exists m such that for every n such that n m holds |s_{1}(n)| r, then |s_{1}| is not convergent or lim|s_{1}| ≠ 0.

(46) s_{1} is convergent iff for every p such that 0 < p there exists n such that for every m such that n m holds |s_{1}(m) − s_{1}(n)| < p.

(47) Suppose s_{1} is convergent. Let given p. Suppose 0 < p. Then there exists n such that for all natural numbers m, l such that n m and n l holds |s_{1}(m) − s_{1}(l)| < p.

(48) If for every n holds |s_{1}(n)| r_{1}(n) and r_{1} is convergent and limr_{1} = 0, then s_{1} is convergent and lims_{1} = 0_{ℂ}.

4. Summable and Absolutely Summable Complex Sequences

Let s_{1}, s_{2} be complex sequences. We say that s_{1} is a subsequence of s_{2} if and only if:

(Def. 9) There exists N_{1} such that s_{1} = s_{2} N_{1}.

Next we state three propositions:

(49) If s_{1} is a subsequence of s_{2}, then ℜ(s_{1}) is a subsequence of ℜ(s_{2}) and ℑ(s_{1}) is a subsequence of ℑ(s_{2}).

(50) If s_{1} is a subsequence of s_{2} and s_{2} is a subsequence of s_{3}, then s_{1} is a subsequence of s_{3}.

(51) If s_{1} is bounded, then there exists s_{2} which is a subsequence of s_{1} and

convergent. Let s_{1} be a complex sequence. We say that s_{1} is summable if and only if:

(Def. 10) (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ} is convergent. Let us observe that there exists a complex sequence which is summable. Let s_{1} be a summable complex sequence. Observe that (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ} is

convergent.

Let us consider s_{1}. We say that s_{1} is absolutely summable if and only if: (Def. 11) |s_{1}| is summable.

One can prove the following proposition

(52) If for every n holds s_{1}(n) = 0_{ℂ}, then s_{1} is absolutely summable. Let us observe that there exists a complex sequence which is absolutely

summable.

Let s_{1} be an absolutely summable complex sequence. Observe that |s_{1}| is summable.

The following proposition is true

(53) If s_{1} is summable, then s_{1} is convergent and lims_{1} = 0_{ℂ}.

One can verify that every complex sequence which is summable is also convergent.

We now state the proposition

(54) If s_{1} is summable, then ℜ(s_{1}) is summable and ℑ(s_{1}) is summable and

∑ s_{1} = ∑ ℜ(s_{1}) + ∑ ℑ(s_{1})i. Let s_{1} be a summable complex sequence. One can verify that ℜ(s_{1}) is sum-

mable and ℑ(s_{1}) is summable.

We now state two propositions:

(55) If s_{2} is summable and s_{3} is summable, then s_{2} + s_{3} is summable and ∑(s_{2} + s_{3}) = ∑ s_{2} + ∑ s_{3}.

(56) If s_{2} is summable and s_{3} is summable, then s_{2} − s_{3} is summable and

∑(s_{2} − s_{3}) = ∑ s_{2} − ∑ s_{3}. Let s_{2}, s_{3} be summable complex sequences. One can check that s_{2} + s_{3} is

summable and s_{2} − s_{3} is summable.

The following proposition is true

(57) If s_{1} is summable, then z s_{1} is summable and ∑(z s_{1}) = z · ∑ s_{1}. Let z be an element of ℂ and let s_{1} be a summable complex sequence. One

can check that z s_{1} is summable.

The following two propositions are true:

(58) If ℜ(s_{1}) is summable and ℑ(s_{1}) is summable, then s_{1} is summable and ∑ s_{1} = ∑ ℜ(s_{1}) + ∑ ℑ(s_{1})i.

(59) If s_{1} is summable, then for every n holds s_{1} ↑ n is summable. Let s_{1} be a summable complex sequence and let n be a natural number.

Note that s_{1} ↑ n is summable.

One can prove the following propositions:

(60) If there exists n such that s_{1} ↑ n is summable, then s_{1} is summable.

(61) If s_{1} is summable, then for every n holds ∑ s_{1} = (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(n)+ ∑(s_{1} ↑ (n + 1)).

(62) (∑_{α=0}^{κ} |s_{1}|(α))_{κ∈ℕ} is upper bounded iff s_{1} is absolutely summable. Let s_{1} be an absolutely summable complex sequence. One can check that

(∑_{α=0}^{κ} |s_{1}|(α))_{κ∈ℕ} is upper bounded.

One can prove the following two propositions:

(63) s_{1} is summable iff for every p such that 0 < p there exists n such that for every m such that n m holds |(∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(m) − (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(n)| < p.

(64) If s_{1} is absolutely summable, then s_{1} is summable.

One can check that every complex sequence which is absolutely summable is also summable.

Let us note that there exists a complex sequence which is absolutely summable.

The following propositions are true:

(65) If |z| < 1, then (z^{κ})_{κ∈ℕ} is summable and ∑((z^{κ})_{κ∈ℕ}) = \frac{1_{ℂ}}{1_{ℂ}−z} .

(66) If |z| < 1 and for every n holds s_{1}(n+1) = z ·s_{1}(n), then s_{1} is summable and ∑ s_{1} = \frac{s_{1}(0)}{1_{ℂ}−z}.

(67) If r_{2} is summable and there exists m such that for every n such that m n holds |s_{3}(n)| r_{2}(n), then s_{3} is absolutely summable.

(68) Suppose for every n holds 0 |s_{2}|(n) and |s_{2}|(n) |s_{3}|(n) and s_{3} is absolutely summable. Then s_{2} is absolutely summable and ∑ |s_{2}| ∑ |s_{3}|.

(69) If for every n holds |s_{1}|(n) > 0 and there exists m such that for every n such that n m holds \frac{|s_{1}|(n+1)}{|s_{1}|(n)} 1, then s_{1} is not absolutely summable.

(70) If for every n holds r_{2}(n) = ^{n} \sqrt{|s_{1}|(n)} and r_{2} is convergent and limr_{2} < 1, then s_{1} is absolutely summable.

(71) If for every n holds r_{2}(n) = ^{n} \sqrt{|s_{1}|(n)} and there exists m such that for every n such that m n holds r_{2}(n) 1, then |s_{1}| is not summable.

(72) If for every n holds r_{2}(n) = ^{n} \sqrt{|s_{1}|(n)} and r_{2} is convergent and limr_{2} > 1, then s_{1} is not absolutely summable.

(73) Suppose |s_{1}| is non-increasing and for every n holds r_{2}(n) = 2^{n} · |s_{1}|(the n-th power of 2). Then s_{1} is absolutely summable if and only if r_{2} is summable.

(74) If p > 1 and for every n such that n 1 holds |s_{1}|(n) = \frac{1}{n^{p}} , then s_{1} is absolutely summable.

(75) If p 1 and for every n such that n 1 holds |s_{1}|(n) = \frac{1}{n^{p}} , then s_{1} is not absolutely summable.

(76) If for every n holds s_{1}(n) ≠ 0_{ℂ} and r_{2}(n) = \frac{|s_{1}|(n+1)}{|s_{1}|(n)} and r_{2} is convergent and limr_{2} < 1, then s_{1} is absolutely summable.

(77) If for every n holds s_{1}(n) ≠ 0_{ℂ} and there exists m such that for every n such that n m holds \frac{|s_{1}|(n+1)}{|s_{1}|(n)} 1, then s_{1} is not absolutely summable.

References

[1] Agnieszka Banachowicz and Anna Winnicka. Complex sequences. Formalized Mathematics, 4(1):121–124, 1993.

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

[3] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 1990.

410 yasunari shidama and artur korniłowicz

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

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

[6] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273–275, 1990.

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

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

[9] Adam Naumowicz. Conjugate sequences, bounded complex sequences and convergent complex sequences. Formalized Mathematics, 6(2):265–268, 1997.

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

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

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

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

The Steinitz Theorem and the Dimension of a Real Linear Space

Jing-Chao Chen Shanghai Jiaotong University Shanghai

Summary. Finite-dimensional real linear spaces are defined. The dimension of such spaces is the cardinality of a basis. Obviously, each two basis have the same cardinality. We prove the Steinitz theorem and the Exchange Lemma. We also investigate some fundamental facts involving the dimension of real linear spaces.

MML Identifier: RLVECT 5.

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

1. Prelimiaries

For simplicity, we follow the rules: V denotes a real linear space, W denotes a subspace of V, x denotes a set, n denotes a natural number, v denotes a vector of V, K_{1}, K_{2} denote linear combinations of V, and X denotes a subset of the carrier of V.

We now state a number of propositions:

(1) If X is linearly independent and the support of K_{1} ⊆ X and the support of K_{2} ⊆ X and ∑ K_{1} = ∑ K_{2}, then K_{1} = K_{2}.

(2) Let V be a real linear space and A be a subset of V. If A is linearly independent, then there exists a basis I of V such that A ⊆ I.

(3) Let L be a linear combination of V and x be a vector of V. Then x ∈ the support of L if and only if there exists v such that x = v and L(v) ≠ 0.

(4) For every finite set X such that n \overline{\overline{X}} there exists a finite subset A of X such that \overline{\overline{A}} = n.

(5) Let L be a linear combination of V, F, G be finite sequences of elements of the carrier of V, and P be a permutation of domF. If G = F · P, then ∑(L F) = ∑(L G).

(6) Let L be a linear combination of V and F be a finite sequence of elements of the carrier of V. If the support of L misses rngF, then ∑(L F) = 0_{V} .

(7) Let F be a finite sequence of elements of the carrier of V. Suppose F is one-to-one. Let L be a linear combination of V. If the support of L ⊆ rngF, then ∑(L F) = ∑ L.

(8) Let L be a linear combination of V and F be a finite sequence of elements of the carrier of V. Then there exists a linear combination K of V such that the support of K = rngF ∩ the support of L and L F = K F.

(9) Let L be a linear combination of V, A be a subset of V, and F be a finite sequence of elements of the carrier of V. Suppose rngF ⊆ the carrier of Lin(A). Then there exists a linear combination K of A such that ∑(L F) = ∑ K.

(10) Let L be a linear combination of V and A be a subset of V. Suppose the support of L ⊆ the carrier of Lin(A). Then there exists a linear combination K of A such that ∑ L = ∑ K.

(11) Let L be a linear combination of V. Suppose the support of L ⊆ the carrier of W. Let K be a linear combination of W. Suppose K = L↾the carrier of W. Then the support of L = the support of K and ∑ L = ∑ K.

(12) Let K be a linear combination of W. Then there exists a linear combination L of V such that the support of K = the support of L and ∑ K = ∑ L.

(13) Let L be a linear combination of V. Suppose the support of L ⊆ the carrier of W. Then there exists a linear combination K of W such that the support of K = the support of L and ∑ K = ∑ L.

(14) For every basis I of V and for every vector v of V holds v ∈ Lin(I).

(15) Let A be a subset of W. Suppose A is linearly independent. Then there exists a subset B of V such that B is linearly independent and B = A.

(16) Let A be a subset of V. Suppose A is linearly independent and A ⊆ the carrier of W. Then there exists a subset B of W such that B is linearly independent and B = A.

(17) For every basis A of W there exists a basis B of V such that A ⊆ B.

(18) Let A be a subset of V. Suppose A is linearly independent. Let v be a vector of V. If v ∈ A, then for every subset B of V such that B = A \ {v} holds v ∉ Lin(B).

(19) Let I be a basis of V and A be a non empty subset of V. Suppose A misses I. Let B be a subset of V. If B = I∪A, then B is linearly-dependent.

(20) For every subset A of V such that A ⊆ the carrier of W holds Lin(A) is a subspace of W.

(21) For every subset A of V and for every subset B of W such that A = B holds Lin(A) = Lin(B).

2. The Steinitz Theorem

Next we state two propositions:

(22) Let A, B be finite subsets of V and v be a vector of V. Suppose v ∈ Lin(A ∪ B) and v ∉ Lin(B). Then there exists a vector w of V such that w ∈ A and w ∈ Lin(((A ∪ B) \ {w}) ∪ {v}).

(23) Let A, B be finite subsets of V. Suppose the RLS structure of V = Lin(A) and B is linearly independent. Then \overline{\overline{B}} \overline{\overline{A}} and there exists a finite subset C of V such that C ⊆ A and \overline{\overline{C}} = \overline{\overline{A}} − \overline{\overline{B}} and the RLS structure of V = Lin(B ∪ C).

3. Finite Dimensional Vector Spaces

Let V be a real linear space. We say that V is finite dimensional if and only if:

(Def. 1) There exists a finite subset of the carrier of V which is a basis of V.

Let us observe that there exists a real linear space which is strict and finite dimensional.

Let V be a real linear space. Let us observe that V is finite dimensional if and only if:

(Def. 2) There exists a finite subset of V which is a basis of V.

We now state several propositions:

(24) If V is finite dimensional, then every basis of V is finite.

(25) If V is finite dimensional, then for every subset A of V such that A is linearly independent holds A is finite.

(26) If V is finite dimensional, then for all bases A, B of V holds \overline{\overline{A}} = \overline{\overline{B}} .

(27) 0_{V} is finite dimensional.

(28) If V is finite dimensional, then W is finite dimensional.

Let V be a real linear space. One can check that there exists a subspace of V which is finite dimensional and strict.

Let V be a finite dimensional real linear space. Observe that every subspace of V is finite dimensional.

Let V be a finite dimensional real linear space. Note that there exists a subspace of V which is strict.

4. The Dimension of a Vector Space

Let V be a real linear space. Let us assume that V is finite dimensional. The functor dim(V) yields a natural number and is defined as follows:

(Def. 3) For every basis I of V holds dim(V) = \overline{\overline{I}} .

We use the following convention: V is a finite dimensional real linear space, W, W_{1}, W_{2} are subspaces of V, and u, v are vectors of V.

Next we state a number of propositions:

(29) dim(W) dim(V).

(30) For every subset A of V such that A is linearly independent holds \overline{\overline{A}} = dim(Lin(A)).

(31) dim(V) = dim(Ω_{V}).

(32) dim(V) = dim(W) iff Ω_{V} = Ω_{W} .

(33) dim(V) = 0 iff Ω_{V} = 0_{V} .

(34) dim(V) = 1 iff there exists v such that v ≠ 0_{V} and Ω_{V} = Lin({v}).

(35) dim(V) = 2 iff there exist u, v such that u ≠ v and {u, v} is linearly independent and Ω_{V} = Lin({u, v}).

(36) dim(W_{1} + W_{2}) + dim(W_{1} ∩ W_{2}) = dim(W_{1}) + dim(W_{2}).

(37) dim(W_{1} ∩ W_{2}) (dim(W_{1}) + dim(W_{2})) − dim(V).

(38) If V is the direct sum of W_{1} and W_{2}, then dim(V) = dim(W_{1})+dim(W_{2}).

(39) n dim(V) iff there exists a strict subspace W of V such that dim(W) =

n. Let V be a finite dimensional real linear space and let n be a natural number.

The functor Sub_{n}(V) yields a set and is defined as follows: (Def. 4) x ∈ Sub_{n}(V) iff there exists a strict subspace W of V such that W = x

and dim(W) = n. The following propositions are true:

(40) If n dim(V), then Sub_{n}(V) is non empty.

(41) If dim(V) < n, then Sub_{n}(V) = ∅.

(42) Sub_{n}(W) ⊆ Sub_{n}(V). the steinitz theorem and the dimension of … 415

References

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

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

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

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

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

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

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

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

[9] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

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

[11] Wojciech A. Trybulec. Basis of real linear space. Formalized Mathematics, 1(5):847–850, 1990.

[12] Wojciech A. Trybulec. Linear combinations in real linear space. Formalized Mathematics, 1(3):581–588, 1990.

[13] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569–573, 1990.

[14] Wojciech A. Trybulec. Operations on subspaces in real linear space. Formalized Mathematics, 1(2):395–399, 1990.

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

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

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

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

[19] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

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

416 jing-chao chen

Euler Circuits and Paths^{1}

Yatsuka Nakamura Shinshu University Nagano

Piotr Rudnicki University of Alberta Edmonton

Summary. We prove the Euler theorem on existence of Euler circuits and paths in multigraphs.

MML Identifier: GRAPH 3.

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

1. Preliminaries

Let D be a set, let T be a non empty set of finite sequences of D, and let S be a non empty subset of T. We see that the element of S is a finite sequence of elements of D.

Let i, j be even integers. One can verify that i − j is even.

We now state two propositions:

(1) For all integers i, j holds i is even iff j is even iff i − j is even.

(2) Let p be a finite sequence and m, n, a be natural numbers. Suppose a ∈ dom⟨p(m), …, p(n)⟩. Then there exists a natural number k such that k ∈ domp and p(k) = ⟨p(m), …, p(n)⟩(a) and k + 1 = m + a and m k and k n.

1This work was partially supported by NSERC Grant OGP9207 and Shinshu Endowment Fund for Information Science.

Let G be a graph. A vertex of G is an element of the vertices of G. For simplicity, we follow the rules: G denotes a graph, v, v_{1}, v_{2} denote vertices

of G, c, c_{1}, c_{2} denote chains of G, p, p_{1}, p_{2} denote paths of G, v_{3}, v_{4}, v_{5} denote finite sequences of elements of the vertices of G, e, X denote sets, and n, m denote natural numbers.

One can prove the following propositions:

(3) If v_{3} is vertex sequence of c, then v_{3} is non empty.

(4) If c is cyclic and v_{3} is vertex sequence of c, then v_{3}(1) = v_{3}(lenv_{3}).

(5) If n ∈ domp and m ∈ domp and n ≠ m, then p(n) ≠ p(m).

(6) ε is a path of G.

(7) If e ∈ the edges of G, then ⟨e⟩ is a path of G.

(8) ⟨p(m), …, p(n)⟩ is a path of G.

(9) Suppose rngp_{1} misses rngp_{2} and v_{4} is vertex sequence of p_{1} and v_{5} is vertex sequence of p_{2} and v_{4}(lenv_{4}) = v_{5}(1). Then p_{1} ^{⌢} p_{2} is a path of G.

(10) p is one-to-one.

(11) If c_{1} ^{⌢} c_{2} is a path of G, then rngc_{1} misses rngc_{2}.

(12) If c = ε, then c is cyclic.

Let G be a graph. Observe that there exists a path of G which is cyclic. Next we state several propositions:

(13) For every cyclic path p of G holds ⟨p(m + 1), …, p(lenp)⟩ ^{⌢} ⟨p(1), …, p(m)⟩ is a cyclic path of G.

(14) If m + 1 ∈ domp, then len(⟨p(m + 1), …, p(lenp)⟩^{⌢} ⟨p(1), …, p(m)⟩) = lenp and rng(⟨p(m + 1), …, p(lenp)⟩ ^{⌢} ⟨p(1), …, p(m)⟩) = rngp and (⟨p(m + 1), …, p(lenp)⟩^{⌢} ⟨p(1), …, p(m)⟩)(1) = p(m + 1).

(15) For every cyclic path p of G such that n ∈ domp there exists a cyclic path p′ of G such that p′(1) = p(n) and lenp′= lenp and rngp′= rngp.

(16) Let s, t be vertices of G. Suppose s = (the source of G)(e) and t = (the target of G)(e). Then ⟨t, s⟩ is vertex sequence of ⟨e⟩.

(17) Suppose e ∈ the edges of G and v_{3} is vertex sequence of c and v_{3}(lenv_{3}) =

(the source of G)(e). Then

(i) c^{⌢} ⟨e⟩ is a chain of G, and (ii) there exists a finite sequence v′_{1} of elements of the vertices of G such

that v′_{1} = v_{3} ⌢⌢ ⟨(the source of G)(e), (the target of G)(e)⟩ and v′_{1} is vertex sequence of c^{⌢} ⟨e⟩ and v′_{1}(1) = v_{3}(1) and v′_{1}(lenv′_{1}) = (the target of G)(e).

(18) Suppose e ∈ the edges of G and v_{3} is vertex sequence of c and v_{3}(lenv_{3}) =

(the target of G)(e). Then

(i) c^{⌢} ⟨e⟩ is a chain of G, and (ii) there exists a finite sequence v′_{1} of elements of the vertices of G such

that v′_{1} = v_{3} ⌢⌢ ⟨(the target of G)(e), (the source of G)(e)⟩ and v′_{1} is vertex

sequence of c^{⌢}⟨e⟩ and v′_{1}(1) = v_{3}(1) and v′_{1}(lenv′_{1}) = (the source of G)(e).

(19) Suppose v_{3} is vertex sequence of c. Let n be a natural number. Suppose

n ∈ domc. Then

(i) v_{3}(n) = (the target of G)(c(n)) and v_{3}(n+1) = (the source of G)(c(n)), or

(ii) v_{3}(n) = (the source of G)(c(n)) and v_{3}(n+1) = (the target of G)(c(n)).

(20) If v_{3} is vertex sequence of c and e ∈ rngc, then (the target of G)(e) ∈

rngv_{3} and (the source of G)(e) ∈ rngv_{3}. Let G be a graph and let X be a set. Then G-VSet(X) is a subset of the

vertices of G.

One can prove the following propositions:

(21) G-VSet(∅) = ∅.

(22) If e ∈ the edges of G and e ∈ X, then G-VSet(X) is non empty.

(23) G is connected if and only if for all v_{1}, v_{2} such that v_{1} ≠ v_{2} there exist c, v_{3} such that c is non empty and v_{3} is vertex sequence of c and v_{3}(1) = v_{1} and v_{3}(lenv_{3}) = v_{2}.

(24) Let G be a connected graph, X be a set, and v be a vertex of G. Suppose X meets the edges of G and v ∉ G-VSet(X). Then there exists a vertex v′ of G and there exists an element e of the edges of G such that v′ ∈ G-VSet(X) but e ∉ X but v′= (the target of G)(e) or v′= (the source of G)(e).

2. Degree of a vertex

Let G be a graph, let v be a vertex of G, and let X be a set. The functor EdgesIn(v, X) yields a subset of the edges of G and is defined as follows:

(Def. 1) For every set e holds e ∈ EdgesIn(v, X) iff e ∈ the edges of G and e ∈ X

and (the target of G)(e) = v. The functor EdgesOut(v, X) yields a subset of the edges of G and is defined as follows:

(Def. 2) For every set e holds e ∈ EdgesOut(v, X) iff e ∈ the edges of G and

e ∈ X and (the source of G)(e) = v. Let G be a graph, let v be a vertex of G, and let X be a set. The functor

EdgesAt(v, X) yields a subset of the edges of G and is defined as follows: (Def. 3) EdgesAt(v, X) = EdgesIn(v, X) ∪ EdgesOut(v, X).

Let G be a finite graph, let v be a vertex of G, and let X be a set. One can check the following observations:

∗ EdgesIn(v, X) is finite, ∗ EdgesOut(v, X) is finite, and

∗ EdgesAt(v, X) is finite.

Let G be a graph, let v be a vertex of G, and let X be an empty set. One can verify the following observations:

∗ EdgesIn(v, X) is empty,

∗ EdgesOut(v, X) is empty, and

∗ EdgesAt(v, X) is empty.

Let G be a graph and let v be a vertex of G. The functor EdgesInv yields a subset of the edges of G and is defined as follows:

(Def. 4) EdgesInv = EdgesIn(v, the edges of G).

The functor EdgesOutv yields a subset of the edges of G and is defined by: (Def. 5) EdgesOutv = EdgesOut(v, the edges of G).

One can prove the following propositions:

(25) EdgesIn(v, X) ⊆ EdgesInv.

(26) EdgesOut(v, X) ⊆ EdgesOutv.

Let G be a finite graph and let v be a vertex of G. Note that EdgesInv is finite and EdgesOutv is finite.

For simplicity, we follow the rules: G denotes a finite graph, v denotes a vertex of G, c denotes a chain of G, v_{3} denotes a finite sequence of elements of the vertices of G, and X_{1}, X_{2} denote sets.

One can prove the following two propositions:

(27) cardEdgesInv = EdgIn(v).

(28) cardEdgesOutv = EdgOut(v).

Let G be a finite graph, let v be a vertex of G, and let X be a set. The functor Degree(v, X) yields a natural number and is defined as follows:

(Def. 6) Degree(v, X) = cardEdgesIn(v, X) + cardEdgesOut(v, X).

The following propositions are true:

(29) The degree of v = Degree(v, the edges of G).

(30) If Degree(v, X) ≠ 0, then EdgesAt(v, X) is non empty.

(31) Suppose e ∈ the edges of G but e ∉ X but v = (the target of G)(e) or v = (the source of G)(e). Then the degree of v ≠ Degree(v, X).

(32) If X_{2} ⊆ X_{1}, then cardEdgesIn(v, X_{1} \ X_{2}) = cardEdgesIn(v, X_{1}) − cardEdgesIn(v, X_{2}).

(33) If X_{2} ⊆ X_{1}, then cardEdgesOut(v, X_{1} \ X_{2}) = cardEdgesOut(v, X_{1}) − cardEdgesOut(v, X_{2}).

(34) If X_{2} ⊆ X_{1}, then Degree(v, X_{1} \ X_{2}) = Degree(v, X_{1}) − Degree(v, X_{2}).

(35) EdgesIn(v, X) = EdgesIn(v, X ∩ the edges of G) and EdgesOut(v, X) = EdgesOut(v, X ∩ the edges of G).

(36) Degree(v, X) = Degree(v, X ∩ the edges of G).

(37) If c is non empty and v_{3} is vertex sequence of c, then v ∈ rngv_{3} iff Degree(v, rngc) ≠ 0.

(38) For every non empty finite connected graph G and for every vertex v of G holds the degree of v ≠ 0.

3. Adding an edge to a graph

Let G be a graph and let v_{1}, v_{2} be vertices of G. The functor AddNewEdge(v_{1}, v_{2}) yielding a strict graph is defined by the conditions (Def. 7).

(Def. 7)(i) The vertices of AddNewEdge(v_{1}, v_{2}) = the vertices of G,

(ii) the edges of AddNewEdge(v_{1}, v_{2}) = (the edges of G) ∪ {the edges of

G}, (iii) the source of AddNewEdge(v_{1}, v_{2}) = (the source of G)+·((the edges of

G)⟼→ . (v_{1})), and (iv) the target of AddNewEdge(v_{1}, v_{2}) = (the target of G)+·((the edges of

G)⟼→ . (v_{2})). Let G be a finite graph and let v_{1}, v_{2} be vertices of G. Observe that

AddNewEdge(v_{1}, v_{2}) is finite.

For simplicity, we adopt the following rules: G is a graph, v, v_{1}, v_{2} are vertices of G, c is a chain of G, p is a path of G, v_{3} is a finite sequence of elements of the vertices of G, v′ is a vertex of AddNewEdge(v_{1}, v_{2}), p′ is a path of AddNewEdge(v_{1}, v_{2}), and v′_{1} is a finite sequence of elements of the vertices of AddNewEdge(v_{1}, v_{2}).

We now state a number of propositions: (39)(i) The edges of G ∈ the edges of AddNewEdge(v_{1}, v_{2}), (ii) the edges of G = (the edges of AddNewEdge(v_{1}, v_{2})) \ {the edges of

G}, (iii) (the source of AddNewEdge(v_{1}, v_{2}))(the edges of G) = v_{1}, and (iv) (the target of AddNewEdge(v_{1}, v_{2}))(the edges of G) = v_{2}.

(40) Suppose e ∈ the edges of G. Then (the source of AddNewEdge(v_{1}, v_{2}))(e) = (the source of G)(e) and (the target of AddNewEdge(v_{1}, v_{2}))(e) = (the target of G)(e).

(41) If v′_{1} = v_{3} and v_{3} is vertex sequence of c, then v′_{1} is vertex sequence of c.

(42) c is a chain of AddNewEdge(v_{1}, v_{2}).

(43) p is a path of AddNewEdge(v_{1}, v_{2}).

(44) If v′= v_{1} and v_{1} ≠ v_{2}, then EdgesIn(v′, X) = EdgesIn(v_{1}, X).

(45) If v′= v_{2} and v_{1} ≠ v_{2}, then EdgesOut(v′, X) = EdgesOut(v_{2}, X).

(46) If v′= v_{1} and v_{1} ≠ v_{2} and the edges of G ∈ X, then EdgesOut(v′, X) = EdgesOut(v_{1}, X) ∪ {the edges of G} and EdgesOut(v_{1}, X) ∩ {the edges of G} = ∅.

(47) If v′ = v_{2} and v_{1} ≠ v_{2} and the edges of G ∈ X, then EdgesIn(v′, X) = EdgesIn(v_{2}, X) ∪ {the edges of G} and EdgesIn(v_{2}, X) ∩ {the edges of G} = ∅.

(48) If v′= v and v ≠ v_{1} and v ≠ v_{2}, then EdgesIn(v′, X) = EdgesIn(v, X).

(49) If v′ = v and v ≠ v_{1} and v ≠ v_{2}, then EdgesOut(v′, X) = EdgesOut(v, X).

(50) If the edges of G ∉ rngp′, then p′ is a path of G.

(51) If the edges of G ∉ rngp′ and v_{3} = v′_{1} and v′_{1} is vertex sequence of p′,

then v_{3} is vertex sequence of p′. Let G be a connected graph and let v_{1}, v_{2} be vertices of G. One can check

that AddNewEdge(v_{1}, v_{2}) is connected.

For simplicity, we adopt the following rules: G is a finite graph, v, v_{1}, v_{2} are vertices of G, v_{3} is a finite sequence of elements of the vertices of G, and v′ is a vertex of AddNewEdge(v_{1}, v_{2}).

We now state two propositions:

(52) If v′= v and v_{1} ≠ v_{2} and v = v_{1} or v = v_{2} and the edges of G ∈ X, then Degree(v′, X) = Degree(v, X) + 1.

(53) If v′= v and v ≠ v_{1} and v ≠ v_{2}, then Degree(v′, X) = Degree(v, X).

4. Some properties of and operations on cycles

The following two propositions are true:

(54) For every cyclic path c of G holds Degree(v, rngc) is even.

(55) Let c be a path of G. Suppose c is non cyclic and v_{3} is vertex sequence of

c. Then Degree(v, rngc) is even if and only if v ≠ v_{3}(1) and v ≠ v_{3}(lenv_{3}). In the sequel G is a graph, v is a vertex of G, and v_{3} is a finite sequence of

elements of the vertices of G.

Let G be a graph. The functor G-CycleSet yields a non empty set of finite sequences of the edges of G and is defined as follows:

(Def. 8) For every set x holds x ∈ G-CycleSet iff x is a cyclic path of G.

One can prove the following propositions:

(56) ε is an element of G-CycleSet.

(57) Let c be an element of G-CycleSet. Suppose v ∈ G-VSet(rngc). Then {c′, c′ ranges over elements of G-CycleSet: rngc′ = rngc ∧ ⋁_{v_{3}} (v_{3} is vertex sequence of c′ ∧ v_{3}(1) = v)} is a non empty subset of G-CycleSet.

Let us consider G, v and let c be an element of G-CycleSet. Let us assume that v ∈ G-VSet(rngc). The functor c_{⟲}^{v} yields an element of G-CycleSet and is defined as follows:

(Def. 9) c_{⟲}^{v} = choose({c′, c′ ranges over elements of G-CycleSet: rngc′= rngc ∧

⋁_{v_{3}} (v_{3} is vertex sequence of c′ ∧ v_{3}(1) = v)}). Let G be a graph and let c_{1}, c_{2} be elements of G-CycleSet. Let us assume

that G-VSet(rngc_{1}) meets G-VSet(rngc_{2}) and rngc_{1} misses rngc_{2}. The functor CatCycles(c_{1}, c_{2}) yields an element of G-CycleSet and is defined as follows:

(Def. 10) There exists a vertex v of G such that v = choose((G-VSet(rngc_{1})) ∩

(G-VSet(rngc_{2}))) and CatCycles(c_{1}, c_{2}) = (c_{1}_{⟲}^{v})^{⌢} c_{2}_{⟲}^{v}. The following proposition is true

(58) Let G be a graph and c_{1}, c_{2} be elements of G-CycleSet. Suppose G-VSet(rngc_{1}) meets G-VSet(rngc_{2}) but rngc_{1} misses rngc_{2} but c_{1} ≠ ε or c_{2} ≠ ε. Then CatCycles(c_{1}, c_{2}) is non empty.

In the sequel G denotes a finite graph, v denotes a vertex of G, and v_{3} denotes a finite sequence of elements of the vertices of G.

Let us consider G, v and let X be a set. Let us assume that Degree(v, X) ≠ 0. The functor X-PathSet(v) yielding a non empty set of finite sequences of the edges of G is defined as follows:

(Def. 11) X-PathSet(v) = {c, c ranges over elements of X^{∗}: c is a path of G ∧ c is

non empty ∧ ⋁_{v_{3}} (v_{3} is vertex sequence of c ∧ v_{3}(1) = v)}. One can prove the following proposition

(59) For every element p of X-PathSet(v) and for every finite set Y such that

Y = the edges of G and Degree(v, X) ≠ 0 holds lenp cardY. Let us consider G, v and let X be a set. Let us assume that for every

vertex v_{1} of G holds Degree(v_{1}, X) is even and Degree(v, X) ≠ 0. The functor X-CycleSetv yielding a non empty subset of G-CycleSet is defined as follows:

(Def. 12) X-CycleSetv = {c, c ranges over elements of G-CycleSet: rngc ⊆ X ∧ c is

non empty ∧ ⋁_{v_{3}} (v_{3} is vertex sequence of c ∧ v_{3}(1) = v)}. Next we state two propositions:

(60) If Degree(v, X) ≠ 0 and for every v holds Degree(v, X) is even, then for every element c of X-CycleSetv holds c is non empty and rngc ⊆ X and v ∈ G-VSet(rngc).

(61) Let G be a finite connected graph and c be an element of G-CycleSet. Suppose rngc ≠ the edges of G and c is non empty. Then {v′, v′ranges over vertices of G: v′ ∈ G-VSet(rngc) ∧ the degree of v′ ≠ Degree(v′, rngc)} is a non empty subset of the vertices of G.

Let G be a finite connected graph and let c be an element of G-CycleSet. Let us assume that rngc ≠ the edges of G and c is non empty. The functor ExtendCyclec yields an element of G-CycleSet and is defined by the condition (Def. 13).

(Def. 13) There exists an element c′of G-CycleSet and there exists a vertex v of G such that v = choose({v′, v′ranges over vertices of G: v′∈ G-VSet(rngc) ∧ the degree of v′ ≠ Degree(v′, rngc)}) and c′= choose(((the edges of G) \ rngc)-CycleSetv) and ExtendCyclec = CatCycles(c, c′).

One can prove the following proposition

(62) Let G be a finite connected graph and c be an element of G-CycleSet. Suppose rngc ≠ the edges of G and c is non empty and for every vertex v of G holds the degree of v is even. Then ExtendCyclec is non empty and cardrngc < cardrngExtendCyclec.

5. Euler circuits and paths

Let G be a graph and let p be a path of G. We say that p is Eulerian if and only if:

(Def. 14) rngp = the edges of G.

We now state three propositions:

(63) Let G be a connected graph, p be a path of G, and v_{3} be a finite sequence of elements of the vertices of G. Suppose p is Eulerian and v_{3} is vertex sequence of p. Then rngv_{3} = the vertices of G.

(64) Let G be a finite connected graph. Then there exists a cyclic path of G which is Eulerian if and only if for every vertex v of G holds the degree of v is even.

(65) Let G be a finite connected graph. Then there exists a path of G which is non cyclic and Eulerian if and only if there exist vertices v_{1}, v_{2} of G such that v_{1} ≠ v_{2} and for every vertex v of G holds the degree of v is even iff v ≠ v_{1} and v ≠ v_{2}.

Acknowledgments

We would like to thank Cz. Byliński for many helpful comments.

References

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

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

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

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

euler circuits and paths 425

[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. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

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

[9] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 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. The correspondence between monotonic many sorted signatures and well-founded graphs. Part I. Formalized Mathematics, 5(4):577– 582, 1996.

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

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

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

[15] Yatsuka Nakamura and Piotr Rudnicki. Vertex sequences induced by chains. Formalized Mathematics, 5(3):297–304, 1996.

[16] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Formalized Mathematics, 5(2):167–172, 1996.

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

[18] Piotr Rudnicki and Andrzej Trybulec. On same equivalents of well-foundedness. Formalized Mathematics, 6(3):339–343, 1997.

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

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

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

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

[23] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

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

426 yatsuka nakamura and piotr rudnicki

Bounding Boxes for Compact Sets in E^{2}

Czesław Byliński^{1} Warsaw University Białystok

Piotr Rudnicki^{2} University of Alberta Edmonton

Summary. We define pseudocompact topological spaces and prove that every compact space is pseudocompact. We also solve an exercise from [16] p.225 that the for a topological space X the following are equivalent:

• Every continuous real map from X is bounded (i.e. X is pseudocompact).

• Every continuous real map from X attains minimum.

• Every continuous real map from X attains maximum. Finally, for a compact set in E^{2} we define its bounding rectangle and introduce a collection of notions associated with the box.

MML Identifier: PSCOMP 1.

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

1. Preliminaries

Let X be a set. Let us observe that X has non empty elements if and only if:

(Def. 1) 0 ∉ X. We introduce X is without zero as a synonym of X has non empty elements. We introduce X has zero as an antonym of X has non empty elements.

Let us observe that ℝ has zero and ℕ has zero.

1This work was partially supported by NSERC Grant OGP9207 and NATO CRG 951368. 2This work was partially supported by NSERC Grant OGP9207 and NATO CRG 951368.

Let us observe that there exists a set which is non empty and without zero and there exists a set which is non empty and has zero.

Let us observe that there exists a subset of ℝ which is non empty and without zero and there exists a subset of ℝ which is non empty and has zero.

Next we state the proposition

(1) For every set F such that F is non empty and ⊆-linear and has non empty elements holds F is centered.

Let F be a set. Note that every family of subsets of F which is non empty and ⊆-linear and has non empty elements is also centered.

Let A, B be sets and let f be a function from A into B. Then rngf is a subset of B.

Let X, Y be non empty sets and let f be a function from X into Y. Note that f^{∘}X is non empty.

Let X, Y be sets and let f be a function from X into Y. The functor ^{−1} f yields a function from 2^{Y} into 2^{X} and is defined by:

(Def. 2) For every subset y of Y holds (^{−1} f)(y) = f^{−1} (y). We now state the proposition

(2) Let X, Y, x be sets, S be a subset of 2^{Y}, and f be a function from X into Y. If x ∈ ⋂((^{−1} f)^{∘}S), then f(x) ∈ ⋂ S.

We follow the rules: p, q, r, r_{1}, r_{2}, s, t are real numbers, s_{1} is a sequence of real numbers, and X, Y are subsets of ℝ.

One can prove the following propositions:

(3) If |r| + |s| = 0, then r = 0 and s = 0.

(4) If r < s and s < t, then |s| < |r| + |t|.

(5) If − s < r and r < s, then |r| < s.

(6) If s_{1} is convergent and non-zero and lims_{1} = 0, then s_{1}^{−1} is non bounded.

(7) rngs_{1} is bounded iff s_{1} is bounded. Next we state four propositions:

(8) Let X be a non empty subset of ℝ and given r. Suppose X is lower bounded. Then r = inf X if and only if the following conditions are satisfied:

(i) for every p such that p ∈ X holds p r, and (ii) for every q such that for every p such that p ∈ X holds p q holds

r q.

(9) Let X be a non empty subset of ℝ and given r. Suppose X is upper bounded. Then r = supX if and only if the following conditions are satisfied:

(i) for every p such that p ∈ X holds p r, and (ii) for every q such that for every p such that p ∈ X holds p q holds

r q.

(10) For every non empty subset X of ℝ and for every subset Y of ℝ such that X ⊆ Y and Y is lower bounded holds inf Y inf X.

(11) For every non empty subset X of ℝ and for every subset Y of ℝ such

that X ⊆ Y and Y is upper bounded holds supX supY. Let X be a subset of ℝ. We say that X has maximum if and only if:

(Def. 3) X is upper bounded and supX ∈ X.

We say that X has minimum if and only if: (Def. 4) X is lower bounded and inf X ∈ X.

One can verify that there exists a subset of ℝ which is non empty, closed, and bounded.

Let R be a family of subsets of ℝ. We say that R is open if and only if: (Def. 5) For every subset X of ℝ such that X ∈ R holds X is open.

We say that R is closed if and only if: (Def. 6) For every subset X of ℝ such that X ∈ R holds X is closed.

Let X be a subset of ℝ. The functor − X yielding a subset of ℝ is defined by:

(Def. 7) − X = {− r : r ∈ X}.

Next we state the proposition

(12) r ∈ X iff − r ∈ − X.

Let X be a non empty subset of ℝ. One can check that − X is non empty. One can prove the following propositions:

(13) − − X = X.

(14) X is upper bounded iff − X is lower bounded.

(15) X is lower bounded iff − X is upper bounded.

(16) For every non empty subset X of ℝ such that X is lower bounded holds inf X = − sup(− X).

(17) For every non empty subset X of ℝ such that X is upper bounded holds supX = − inf(− X).

(18) X is closed iff − X is closed.

Let X be a subset of ℝ and let p be a real number. The functor p + X yields a subset of ℝ and is defined by:

(Def. 8) p + X = {p + r : r ∈ X}.

One can prove the following proposition

(19) r ∈ X iff s + r ∈ s + X.

Let X be a non empty subset of ℝ and let s be a real number. Observe that s + X is non empty.

One can prove the following propositions:

(20) X = 0 + X.

(21) s + (t + X) = (s + t) + X.

(22) X is upper bounded iff s + X is upper bounded.

(23) X is lower bounded iff s + X is lower bounded.

(24) For every non empty subset X of ℝ such that X is lower bounded holds inf(s + X) = s + inf X.

(25) For every non empty subset X of ℝ such that X is upper bounded holds sup(s + X) = s + supX.

(26) X is closed iff s + X is closed.

Let X be a subset of ℝ. The functor InvX yielding a subset of ℝ is defined by:

(Def. 9) InvX = \{\frac{1}{r} : r ∈ X\}.

The following proposition is true

(27) For every without zero subset X of ℝ such that r ≠ 0 holds r ∈ X iff

\frac{1}{r} ∈ InvX. Let X be a non empty without zero subset of ℝ. One can verify that InvX

is non empty and without zero.

Let X be a without zero subset of ℝ. One can verify that InvX is without zero.

The following propositions are true:

(28) For every without zero subset X of ℝ holds InvInvX = X.

(29) For every without zero subset X of ℝ such that X is closed and bounded holds InvX is closed.

(30) For every family Z of subsets of ℝ such that Z is closed holds ⋂ Z is

closed. Let X be a subset of ℝ. The functor \overline{X} yielding a subset of ℝ is defined by:

(Def. 10) \overline{X} = ⋂\{A, A ranges over elements of 2^{ℝ}: X ⊆ A ∧ A is closed\}. Let X be a subset of ℝ. Observe that \overline{X} is closed. Next we state several propositions:

(31) For every closed subset Y of ℝ such that X ⊆ Y holds \overline{X} ⊆ Y.

(32) X ⊆ \overline{X}.

(33) X is closed iff X = \overline{X}.

(34) \overline{∅_{ℝ}} = ∅.

(35) \overline{Ω_{ℝ}} = ℝ.

(36) \overline{X} = \overline{\overline{X}}.

(37) If X ⊆ Y, then \overline{X} ⊆ \overline{Y} .

(38) r ∈ \overline{X} iff for every open subset O of ℝ such that r ∈ O holds O ∩ X is non empty.

(39) If r ∈ \overline{X}, then there exists s_{1} such that rngs_{1} ⊆ X and s_{1} is convergent and lims_{1} = r.

2. Functions into Reals

Let A be a set, let f be a function from A into ℝ, and let a be a set. Then f(a) is a real number.

Let X be a set and let f be a function from X into ℝ. We say that f is lower bounded if and only if:

(Def. 11) f^{∘}X is lower bounded.

We say that f is upper bounded if and only if: (Def. 12) f^{∘}X is upper bounded.

Let X be a set and let f be a function from X into ℝ. We say that f is bounded if and only if:

(Def. 13) f is lower bounded and upper bounded.

We say that f has maximum if and only if: (Def. 14) f^{∘}X has maximum.

We say that f has minimum if and only if: (Def. 15) f^{∘}X has minimum.

Let X be a set. One can check that every function from X into ℝ which is bounded is also lower bounded and upper bounded and every function from X into ℝ which is lower bounded and upper bounded is also bounded.

Let X be a set and let f be a function from X into ℝ. The functor − f yields a function from X into ℝ and is defined as follows:

(Def. 16) For every set p such that p ∈ X holds (− f)(p) = − f(p).

The following propositions are true:

(40) For all sets X, A and for every function f from X into ℝ holds (− f)^{∘}A = − f^{∘}A.

(41) For every set X and for every function f from X into ℝ holds − − f = f.

(42) For every non empty set X and for every function f from X into ℝ holds f has minimum iff − f has maximum.

(43) For every non empty set X and for every function f from X into ℝ holds f has maximum iff − f has minimum.

(44) For every set X and for every subset A of ℝ and for every function f

from X into ℝ holds (− f)^{−1} (A) = f^{−1} (− A). Let X be a set, let r be a real number, and let f be a function from X into

ℝ. The functor r + f yielding a function from X into ℝ is defined as follows: (Def. 17) For every set p such that p ∈ X holds (r + f)(p) = r + f(p).

One can prove the following two propositions:

(45) For all sets X, A and for every function f from X into ℝ and for every real number s holds (s + f)^{∘}A = s + f^{∘}A.

(46) For every set X and for every subset A of ℝ and for every function f

from X into ℝ and for every s holds (s + f)^{−1} (A) = f^{−1} (− s + A). Let X be a set and let f be a function from X into ℝ. The functor Invf

yields a function from X into ℝ and is defined by: (Def. 18) For every set p such that p ∈ X holds (Invf)(p) = \frac{1}{f(p)}.

We now state the proposition

(47) Let X be a set, A be a without zero subset of ℝ, and f be a function from X into ℝ. If 0 ∉ rngf, then (Invf)^{−1} (A) = f^{−1} (InvA).

3. Real maps

Let T be a 1-sorted structure. (Def. 19) A function from the carrier of T into ℝ is called a real map of T.

Let T be a non empty 1-sorted structure. Note that there exists a real map of T which is bounded.

In this article we present several logical schemes. The scheme NonUniqExRF deals with a non empty topological structure A and a binary predicate P, and states that:

There exists a real map f of A such that for every element x of the carrier of A holds P[x, f(x)]

provided the parameters meet the following requirement:

• For every set x such that x ∈ the carrier of A there exists r such that P[x, r].

The scheme LambdaRF deals with a non empty topological structure A and a unary functor F yielding a real number, and states that:

There exists a real map f of A such that for every element x of the carrier of A holds f(x) = F(x)

for all values of the parameters.

Let T be a 1-sorted structure, let f be a real map of T, and let P be a set. Then f^{−1} (P) is a subset of T.

Let T be a 1-sorted structure and let f be a real map of T. The functor inf f yielding a real number is defined by:

(Def. 20) inf f = inf(f^{∘}(the carrier of T)).

The functor supf yields a real number and is defined by: (Def. 21) supf = sup(f^{∘}(the carrier of T)).

Next we state three propositions:

(48) Let T be a non empty topological space and f be a lower bounded real map of T. Then r = inf f if and only if the following conditions are satisfied:

(i) for every point p of T holds f(p) r, and (ii) for every real number q such that for every point p of T holds f(p) q

holds r q.

(49) Let T be a non empty topological space and f be an upper bounded real map of T. Then r = supf if and only if the following conditions are satisfied:

(i) for every point p of T holds f(p) r, and (ii) for every real number q such that for every point p of T holds f(p) q

holds r q.

(50) For every non empty 1-sorted structure T and for every bounded real

map f of T holds inf f supf. Let T be a 1-sorted structure and let f be a real map of T. The functor − f

yielding a real map of T is defined by: (Def. 22) − f = − f.

Let T be a 1-sorted structure, let r be a real number, and let f be a real map of T. The functor r + f yields a real map of T and is defined by:

(Def. 23) r + f = r + f.

Let T be a 1-sorted structure and let f be a real map of T. The functor Invf yields a real map of T and is defined by:

(Def. 24) Invf = Invf.

Let T be a topological structure and let f be a real map of T. We say that f is continuous if and only if:

(Def. 25) For every subset Y of ℝ such that Y is closed holds f^{−1} (Y) is closed.

Let T be a non empty topological space. Note that there exists a real map of T which is continuous.

Let T be a non empty topological space and let S be a non empty subspace of T. One can check that there exists a real map of S which is continuous.

In the sequel T is a topological space and f is a real map of T. Next we state several propositions:

(51) f is continuous iff for every subset Y of ℝ such that Y is open holds f^{−1} (Y) is open.

(52) If f is continuous, then − f is continuous.

(53) If f is continuous, then r + f is continuous.

(54) If f is continuous and 0 ∉ rngf, then Invf is continuous.

(55) For every family R of subsets of ℝ such that f is continuous and R is open holds (^{−1} f)^{∘}R is open.

(56) For every family R of subsets of ℝ such that f is continuous and R is

closed holds (^{−1} f)^{∘}R is closed. Let T be a non empty topological space, let X be a subset of T, and let f

be a real map of T. The functor f ↾ X yielding a real map of T ↾X is defined as follows:

(Def. 26) f ↾ X = f↾X.

Let T be a non empty topological space. One can check that there exists a subset of T which is compact and non empty.

Let T be a non empty topological space, let f be a continuous real map of T, and let X be a compact non empty subset of T. Note that f ↾ X is continuous.

Let T be a non empty topological space and let P be a compact non empty subset of T. Note that T ↾P is compact.

4. Pseudocompact spaces

We now state two propositions:

(57) Let T be a non empty topological space. Then for every real map f of T such that f is continuous holds f has maximum if and only if for every real map f of T such that f is continuous holds f has minimum.

(58) Let T be a non empty topological space. Then for every real map f of T such that f is continuous holds f is bounded if and only if for every real map f of T such that f is continuous holds f has maximum.

Let T be a topological space. We say that T is pseudocompact if and only if:

(Def. 27) For every real map f of T such that f is continuous holds f is bounded.

Let us mention that every non empty topological space which is compact is also pseudocompact.

Let us mention that there exists a topological space which is compact and non empty.

Let T be a pseudocompact non empty topological space. One can check that every real map of T which is continuous is also bounded and has maximum and minimum.

We now state two propositions:

(59) Let T be a non empty topological space, X, Y be non empty compact subsets of T, and f be a continuous real map of T. If X ⊆ Y, then inf(f ↾ Y) inf(f ↾ X).

(60) Let T be a non empty topological space, X, Y be non empty compact subsets of T, and f be a continuous real map of T. If X ⊆ Y, then sup(f ↾ X) sup(f ↾ Y).

5. Bounding boxes for compact sets in E^{2}

Let n be a natural number and let p_{1}, p_{2} be points of E_{T}^{n}. Note that L(p_{1}, p_{2}) is compact.

One can prove the following proposition

(61) For every natural number n and for all compact subsets X, Y of E_{T}^{n}

holds X ∩ Y is compact. In the sequel p is a point of E_{T}^{2}, P is a subset of E_{T}^{2}, and X is a non empty

compact subset of E_{T}^{2}.

The real map proj1 of E_{T}^{2} is defined as follows: (Def. 28) For every point p of E_{T}^{2} holds (proj1)(p) = p_{1}.

The real map proj2 of E_{T}^{2} is defined by: (Def. 29) For every point p of E_{T}^{2} holds (proj2)(p) = p_{2}.

One can prove the following propositions:

(62) (proj1)^{−1} (]r, s[) = {[r_{1}, r_{2}] : r < r_{1} ∧ r_{1} < s}.

(63) For all r, s such that P = {[r_{1}, r_{2}] : r < r_{1} ∧ r_{1} < s} holds P is open.

(64) (proj2)^{−1} (]r, s[) = {[r_{1}, r_{2}] : r < r_{2} ∧ r_{2} < s}.

(65) For all r, s such that P = {[r_{1}, r_{2}] : r < r_{2} ∧ r_{2} < s} holds P is open. One can verify that proj1 is continuous and proj2 is continuous. One can prove the following two propositions:

(66) For every non empty subset X of E_{T}^{2} and for every point p of E_{T}^{2} such that p ∈ X holds (proj1 ↾ X)(p) = p_{1}.

(67) For every non empty subset X of E_{T}^{2} and for every point p of E_{T}^{2} such

that p ∈ X holds (proj2 ↾ X)(p) = p_{2}. Let X be a non empty subset of E_{T}^{2}. The functor W-boundX yielding a real

number is defined by: (Def. 30) W-boundX = inf(proj1 ↾ X).

The functor N-boundX yielding a real number is defined as follows: (Def. 31) N-boundX = sup(proj2 ↾ X).

The functor E-boundX yielding a real number is defined by: (Def. 32) E-boundX = sup(proj1 ↾ X).

The functor S-boundX yielding a real number is defined by: (Def. 33) S-boundX = inf(proj2 ↾ X).

We now state the proposition

(68) If p ∈ X, then W-boundX p_{1} and p_{1} E-boundX and S-boundX

p_{2} and p_{2} N-boundX. Let X be a non empty subset of E_{T}^{2}. The functor SW-cornerX yields a point

of E_{T}^{2} and is defined as follows: (Def. 34) SW-cornerX = [W-boundX, S-boundX].

The functor NW-cornerX yielding a point of E_{T}^{2} is defined as follows: (Def. 35) NW-cornerX = [W-boundX, N-boundX].

The functor NE-cornerX yields a point of E_{T}^{2} and is defined as follows: (Def. 36) NE-cornerX = [E-boundX, N-boundX].

The functor SE-cornerX yields a point of E_{T}^{2} and is defined as follows: (Def. 37) SE-cornerX = [E-boundX, S-boundX].

Let X be a non empty subset of E_{T}^{2}. The functor W-mostX yielding a subset of E_{T}^{2} is defined as follows:

(Def. 38) W-mostX = L(SW-cornerX, NW-cornerX) ∩ X.

The functor N-mostX yielding a subset of E_{T}^{2} is defined as follows: (Def. 39) N-mostX = L(NW-cornerX, NE-cornerX) ∩ X.

The functor E-mostX yields a subset of E_{T}^{2} and is defined by: (Def. 40) E-mostX = L(SE-cornerX, NE-cornerX) ∩ X.

The functor S-mostX yielding a subset of E_{T}^{2} is defined by: (Def. 41) S-mostX = L(SW-cornerX, SE-cornerX) ∩ X.

Let X be a non empty compact subset of E_{T}^{2}. One can check the following observations:

∗ W-mostX is non empty and compact,

∗ N-mostX is non empty and compact,

∗ E-mostX is non empty and compact, and

∗ S-mostX is non empty and compact.

Let X be a non empty compact subset of E_{T}^{2}. The functor W-minX yielding a point of E_{T}^{2} is defined by:

(Def. 42) W-minX = [W-boundX, inf(proj2 ↾ W-mostX)].

The functor W-maxX yielding a point of E_{T}^{2} is defined by: (Def. 43) W-maxX = [W-boundX, sup(proj2 ↾ W-mostX)].

The functor N-minX yielding a point of E_{T}^{2} is defined by: (Def. 44) N-minX = [inf(proj1 ↾ N-mostX), N-boundX].

The functor N-maxX yielding a point of E_{T}^{2} is defined by: (Def. 45) N-maxX = [sup(proj1 ↾ N-mostX), N-boundX].

The functor E-maxX yields a point of E_{T}^{2} and is defined by:

(Def. 46) E-maxX = [E-boundX, sup(proj2 ↾ E-mostX)].

The functor E-minX yields a point of E_{T}^{2} and is defined by: (Def. 47) E-minX = [E-boundX, inf(proj2 ↾ E-mostX)].

The functor S-maxX yields a point of E_{T}^{2} and is defined by: (Def. 48) S-maxX = [sup(proj1 ↾ S-mostX), S-boundX].

The functor S-minX yielding a point of E_{T}^{2} is defined by: (Def. 49) S-minX = [inf(proj1 ↾ S-mostX), S-boundX].

Next we state a number of propositions:

(69) (SW-cornerX)_{1} = W-boundX and (W-minX)_{1} = W-boundX and (W-maxX)_{1} = W-boundX and (NW-cornerX)_{1} = W-boundX.

(70) (SW-cornerX)_{1} = (NW-cornerX)_{1} and (SW-cornerX)_{1} = (W-minX)_{1} and (SW-cornerX)_{1} = (W-maxX)_{1} and (W-minX)_{1} = (W-maxX)_{1} and (W-minX)_{1} = (NW-cornerX)_{1} and (W-maxX)_{1} = (NW-cornerX)_{1}.

(71) (SW-cornerX)_{2} = S-boundX and (W-minX)_{2} = inf(proj2 ↾ W-mostX) and (W-maxX)_{2} = sup(proj2 ↾ W-mostX) and (NW-cornerX)_{2} = N-boundX.

(72) (SW-cornerX)_{2} (W-minX)_{2} and (SW-cornerX)_{2} (W-maxX)_{2} and (SW-cornerX)_{2} (NW-cornerX)_{2} and (W-minX)_{2} (W-maxX)_{2} and (W-minX)_{2} (NW-cornerX)_{2} and (W-maxX)_{2} (NW-cornerX)_{2}.

(73) If p ∈ W-mostX, then p_{1} = (W-minX)_{1} and (W-minX)_{2} p_{2} and p_{2} (W-maxX)_{2}.

(74) W-mostX ⊆ L(W-minX, W-maxX).

(75) L(W-minX, W-maxX) ⊆ L(SW-cornerX, NW-cornerX).

(76) W-minX ∈ W-mostX and W-maxX ∈ W-mostX.

(77) L(SW-cornerX, W-minX) ∩ X = {W-minX} and L(W-maxX, NW-cornerX) ∩ X = {W-maxX}.

(78) If W-minX = W-maxX, then W-mostX = {W-minX}.

(79) (NW-cornerX)_{2} = N-boundX and (N-minX)_{2} = N-boundX and (N-maxX)_{2} = N-boundX and (NE-cornerX)_{2} = N-boundX.

(80) (NW-cornerX)_{2} = (NE-cornerX)_{2} and (NW-cornerX)_{2} = (N-minX)_{2} and (NW-cornerX)_{2} = (N-maxX)_{2} and (N-minX)_{2} = (N-maxX)_{2} and (N-minX)_{2} = (NE-cornerX)_{2} and (N-maxX)_{2} = (NE-cornerX)_{2}.

(81) (NW-cornerX)_{1} = W-boundX and (N-minX)_{1} = inf(proj1 ↾ N-mostX) and (N-maxX)_{1} = sup(proj1 ↾ N-mostX) and (NE-cornerX)_{1} = E-boundX.

(82) (NW-cornerX)_{1} (N-minX)_{1} and (NW-cornerX)_{1} (N-maxX)_{1} and (NW-cornerX)_{1} (NE-cornerX)_{1} and (N-minX)_{1} (N-maxX)_{1} and (N-minX)_{1} (NE-cornerX)_{1} and (N-maxX)_{1} (NE-cornerX)_{1}.

(83) If p ∈ N-mostX, then p_{2} = (N-minX)_{2} and (N-minX)_{1} p_{1} and p_{1} (N-maxX)_{1}.

(84) N-mostX ⊆ L(N-minX, N-maxX).

(85) L(N-minX, N-maxX) ⊆ L(NW-cornerX, NE-cornerX).

(86) N-minX ∈ N-mostX and N-maxX ∈ N-mostX.

(87) L(NW-cornerX, N-minX) ∩ X = {N-minX} and L(N-maxX, NE-cornerX) ∩ X = {N-maxX}.

(88) If N-minX = N-maxX, then N-mostX = {N-minX}.

(89) (SE-cornerX)_{1} = E-boundX and (E-minX)_{1} = E-boundX and (E-maxX)_{1} = E-boundX and (NE-cornerX)_{1} = E-boundX.

(90) (SE-cornerX)_{1} = (NE-cornerX)_{1} and (SE-cornerX)_{1} = (E-minX)_{1} and (SE-cornerX)_{1} = (E-maxX)_{1} and (E-minX)_{1} = (E-maxX)_{1} and (E-minX)_{1} = (NE-cornerX)_{1} and (E-maxX)_{1} = (NE-cornerX)_{1}.

(91) (SE-cornerX)_{2} = S-boundX and (E-minX)_{2} = inf(proj2 ↾ E-mostX) and (E-maxX)_{2} = sup(proj2 ↾ E-mostX) and (NE-cornerX)_{2} = N-boundX.

(92) (SE-cornerX)_{2} (E-minX)_{2} and (SE-cornerX)_{2} (E-maxX)_{2} and (SE-cornerX)_{2} (NE-cornerX)_{2} and (E-minX)_{2} (E-maxX)_{2} and (E-minX)_{2} (NE-cornerX)_{2} and (E-maxX)_{2} (NE-cornerX)_{2}.

(93) If p ∈ E-mostX, then p_{1} = (E-minX)_{1} and (E-minX)_{2} p_{2} and p_{2} (E-maxX)_{2}.

(94) E-mostX ⊆ L(E-minX, E-maxX).

(95) L(E-minX, E-maxX) ⊆ L(SE-cornerX, NE-cornerX).

(96) E-minX ∈ E-mostX and E-maxX ∈ E-mostX.

(97) L(SE-cornerX, E-minX) ∩ X = {E-minX} and L(E-maxX, NE-cornerX) ∩ X = {E-maxX}.

(98) If E-minX = E-maxX, then E-mostX = {E-minX}.

(99) (SW-cornerX)_{2} = S-boundX and (S-minX)_{2} = S-boundX and (S-maxX)_{2} = S-boundX and (SE-cornerX)_{2} = S-boundX.

(100) (SW-cornerX)_{2} = (SE-cornerX)_{2} and (SW-cornerX)_{2} = (S-minX)_{2} and (SW-cornerX)_{2} = (S-maxX)_{2} and (S-minX)_{2} = (S-maxX)_{2} and (S-minX)_{2} = (SE-cornerX)_{2} and (S-maxX)_{2} = (SE-cornerX)_{2}.

(101) (SW-cornerX)_{1} = W-boundX and (S-minX)_{1} = inf(proj1 ↾ S-mostX) and (S-maxX)_{1} = sup(proj1 ↾ S-mostX) and (SE-cornerX)_{1} = E-boundX.

(102) (SW-cornerX)_{1} (S-minX)_{1} and (SW-cornerX)_{1} (S-maxX)_{1} and (SW-cornerX)_{1} (SE-cornerX)_{1} and (S-minX)_{1} (S-maxX)_{1} and (S-minX)_{1} (SE-cornerX)_{1} and (S-maxX)_{1} (SE-cornerX)_{1}.

bounding boxes for compact sets in … 439

(103) If p ∈ S-mostX, then p_{2} = (S-minX)_{2} and (S-minX)_{1} p_{1} and p_{1} (S-maxX)_{1}.

(104) S-mostX ⊆ L(S-minX, S-maxX).

(105) L(S-minX, S-maxX) ⊆ L(SW-cornerX, SE-cornerX).

(106) S-minX ∈ S-mostX and S-maxX ∈ S-mostX.

(107) L(SW-cornerX, S-minX) ∩ X = {S-minX} and L(S-maxX, SE-cornerX) ∩ X = {S-maxX}.

(108) If S-minX = S-maxX, then S-mostX = {S-minX}.

(109) If W-maxX = N-minX, then W-maxX = NW-cornerX.

(110) If N-maxX = E-maxX, then N-maxX = NE-cornerX.

(111) If E-minX = S-maxX, then E-minX = SE-cornerX.

(112) If S-minX = W-minX, then S-minX = SW-cornerX.

References

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

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

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

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

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

[6] Agata Darmochwał. Families of subsets, subspaces and mappings in topological spaces. Formalized Mathematics, 1(2):257–261, 1990.

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

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

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

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

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

[12] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273–275, 1990.

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

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

[15] Jarosław Kotowicz. The limit of a real function at infinity. Formalized Mathematics, 2(1):17–28, 1991.

[16] M.G. Murdeshwar. General Topology. Wiley Eastern, 1990.

[17] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Formalized Mathematics, 3(2):151–160, 1992.

[18] Bogdan Nowak and Andrzej Trybulec. Hahn-Banach theorem. Formalized Mathematics, 4(1):29–34, 1993.

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

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

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

440 czesław byliński and piotr rudnicki

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

[23] Piotr Rudnicki and Andrzej Trybulec. On same equivalents of well-foundedness. Formalized Mathematics, 6(3):339–343, 1997.

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

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

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

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

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

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

[30] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

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

The Scott Topology. Part II^{1}

Czesław Byliński Warsaw University Białystok

Piotr Rudnicki University of Alberta Edmonton

Summary. Mizar formalization of pp. 105–108 of [15] which continues [34]. We found a simplification for the proof of Corollary 1.15, in the last case, see the proof in the Mizar article for details.

MML Identifier: WAYBEL14.

The terminology and notation used in this paper are introduced in the following articles: [30], [37], [10], [2], [25], [14], [29], [38], [8], [9], [35], [3], [1], [36], [27], [39], [13], [26], [31], [17], [28], [18], [12], [4], [16], [41], [19], [20], [33], [6], [32], [5], [11], [21], [7], [40], [23], [24], [22], and [34].

1. Preliminaries

The following propositions are true:

(1) Let X be a set and F be a finite family of subsets of X. Then there exists a finite family G of subsets of X such that G ⊆ F and ⋃ G = ⋃ F and for every subset g of X such that g ∈ G holds g ⊈ ⋃(G \ {g}).

(2) Let S be a 1-sorted structure and X be a subset of the carrier of S. Then − X = the carrier of S if and only if X is empty.

(3) Let R be an antisymmetric transitive non empty relational structure with g.l.b.’s and x, y be elements of R. Then ↓(x ⊓ y) = ↓x ∩ ↓y.

(4) Let R be an antisymmetric transitive non empty relational structure with l.u.b.’s and x, y be elements of R. Then ↑(x ⊔ y) = ↑x ∩ ↑y.

1This work was partially supported by NSERC Grant OGP9207 and NATO CRG 951368.

(5) Let L be a complete antisymmetric non empty relational structure and X be a lower subset of L. If supX ∈ X, then X = ↓supX.

(6) Let L be a complete antisymmetric non empty relational structure and X be an upper subset of L. If inf X ∈ X, then X = ↑inf X.

(7) Let R be a non empty reflexive transitive relational structure and x, y be elements of R. Then x ≪ y if and only if ↑y ⊆ ↑↑x.

(8) Let R be a non empty reflexive transitive relational structure and x, y be elements of R. Then x ≪ y if and only if ↓x ⊆ ↓↓y.

(9) Let R be a complete reflexive antisymmetric non empty relational structure and x be an element of R. Then sup↓↓x x and x inf ↑↑x.

(10) For every lower-bounded antisymmetric non empty relational structure L holds ↑(⊥_{L}) = the carrier of L.

(11) For every upper-bounded antisymmetric non empty relational structure L holds ↓(⊤_{L}) = the carrier of L.

(12) For every poset P with l.u.b.’s and for all elements x, y of P holds ↑↑x ⊔ ↑↑y ⊆ ↑(x ⊔ y).

(13) For every poset P with g.l.b.’s and for all elements x, y of P holds ↓↓x ⊓ ↓↓y ⊆ ↓(x ⊓ y).

(14) Let R be a non empty poset with l.u.b.’s and l be an element of R. Then l is co-prime if and only if for all elements x, y of R such that l x ⊔ y holds l x or l y.

(15) For every complete non empty poset P and for every non empty subset V of P holds ↓inf V = ⋂{↓u, u ranges over elements of P: u ∈ V }.

(16) For every complete non empty poset P and for every non empty subset

V of P holds ↑supV = ⋂{↑u, u ranges over elements of P: u ∈ V }. Let L be a sup-semilattice and let x be an element of L. Note that compactbelow(x) is directed. We now state four propositions:

(17) Let T be a non empty topological space, S be an irreducible subset of T, and V be an element of ⟨the topology of T, ⊆⟩. If V = − S, then V is prime.

(18) Let T be a non empty topological space and x, y be elements of ⟨the topology of T, ⊆⟩. Then x ⊔ y = x ∪ y and x ⊓ y = x ∩ y.

(19) Let T be a non empty topological space and V be an element of ⟨the topology of T, ⊆⟩. Then V is prime if and only if for all elements X, Y of ⟨the topology of T, ⊆⟩ such that X ∩ Y ⊆ V holds X ⊆ V or Y ⊆ V.

(20) Let T be a non empty topological space and V be an element of ⟨the topology of T, ⊆⟩. Then V is co-prime if and only if for all elements X, Y of ⟨the topology of T, ⊆⟩ such that V ⊆ X ∪ Y holds V ⊆ X or V ⊆ Y.

Let T be a non empty topological space. One can check that ⟨the topology of T, ⊆⟩ is distributive.

The following propositions are true:

(21) Let T be a non empty topological space, L be a TopLattice, t be a point of T, l be a point of L, and X be a family of subsets of the carrier of L. Suppose the topological structure of T = the topological structure of L and t = l and X is a basis of l. Then X is a basis of t.

(22) Let L be a TopLattice and x be an element of L. Suppose that for every subset X of L such that X is open holds X is upper. Then ↑x is compact.

2. The Scott topology^{2}

For simplicity, we use the following convention: L is a complete Scott TopLattice, x is an element of L, X, Y are subsets of L, V, W are elements of ⟨σ(L), ⊆⟩, and V_{1} is a subset of ⟨σ(L), ⊆⟩.

Let L be a complete lattice. One can check that σ(L) is non empty.

The following four propositions are true:

(23) σ(L) = the topology of L.

(24) X ∈ σ(L) iff X is open.

(25) For every filtered subset X of L such that V_{1} = {− ↓x : x ∈ X} holds V_{1} is directed.

(26) If X is open and x ∈ X, then inf X ≪ x.

Let R be a non empty reflexive relational structure and let f be a map from [: R, R:] into R. We say that f is jointly Scott-continuous if and only if the condition (Def. 1) is satisfied.

(Def. 1) Let T be a non empty topological space. Suppose the topological structure of T = ConvergenceSpace(the Scott convergence of R). Then there exists a map f_{1} from [: T, T :] into T such that f_{1} = f and f_{1} is continuous.

One can prove the following propositions:

(27) If V = X, then V is co-prime iff X is filtered and upper.

(28) If V = X and there exists x such that X = − ↓x, then V is prime and V ≠ the carrier of L.

(29) If V = X and ⊔_{L} is jointly Scott-continuous and V is prime and V ≠ the carrier of L, then there exists x such that X = − ↓x.

(30) If L is continuous, then ⊔_{L} is jointly Scott-continuous.

(31) If ⊔_{L} is jointly Scott-continuous, then L is sober.

2σ(L) = sigma L, as defined in [34, p. 316, Def. 12] and ⊔_{L} = sup op(L), as defined in [21, p. 163, Def. 5].

(32) If L is continuous, then L is compact, locally-compact, sober, and Baire.

(33) If L is continuous and X ∈ σ(L), then X = ⋃{↑↑x : x ∈ X}.

(34) If for every X such that X ∈ σ(L) holds X = ⋃{↑↑x : x ∈ X}, then L is continuous.

(35) If L is continuous, then there exists a basis B of x such that for every X such that X ∈ B holds X is open and filtered.

(36) If L is continuous, then ⟨σ(L), ⊆⟩ is continuous.

(37) Suppose for every x there exists a basis B of x such that for every Y such that Y ∈ B holds Y is open and filtered and ⟨σ(L), ⊆⟩ is continuous. Then x = ⨆_{L}{inf X : x ∈ X ∧ X ∈ σ(L)}.

(38) If for every x holds x = ⨆_{L}{inf X : x ∈ X ∧ X ∈ σ(L)}, then L is continuous.

(39) The following statements are equivalent

(i) for every x there exists a basis B of x such that for every Y such that Y ∈ B holds Y is open and filtered,

(ii) for every V there exists V_{1} such that V = supV_{1} and for every W such

that W ∈ V_{1} holds W is co-prime.

(40) For every V there exists V_{1} such that V = supV_{1} and for every W such that W ∈ V_{1} holds W is co-prime and ⟨σ(L), ⊆⟩ is continuous if and only if ⟨σ(L), ⊆⟩ is completely-distributive.

(41) ⟨σ(L), ⊆⟩ is completely-distributive iff ⟨σ(L), ⊆⟩ is continuous and (⟨σ(L), ⊆⟩)^{op} is continuous.

(42) If L is algebraic, then there exists a basis B of L such that B = {↑x : x ∈ the carrier of CompactSublatt(L)}.

(43) Given a basis B of L such that B = {↑x : x ∈ the carrier of CompactSublatt(L)}. Then ⟨σ(L), ⊆⟩ is algebraic and for every V there exists V_{1} such that V = supV_{1} and for every W such that W ∈ V_{1} holds W is co-prime.

(44) Suppose ⟨σ(L), ⊆⟩ is algebraic and for every V there exists V_{1} such that V = supV_{1} and for every W such that W ∈ V_{1} holds W is co-prime. Then there exists a basis B of L such that B = {↑x : x ∈ the carrier of CompactSublatt(L)}.

(45) If there exists a basis B of L such that B = {↑x : x ∈ the carrier of CompactSublatt(L)}, then L is algebraic.

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. Complete lattices. Formalized Mathematics, 2(5):719–725, 1991.

the scott topology. part ii 445

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

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

[6] Grzegorz Bancerek. Duality in relation structures. Formalized Mathematics, 6(2):227–232, 1997.

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

[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. Galois connections. Formalized Mathematics, 6(1):131–143, 1997.

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

[13] Agata Darmochwał. Families of subsets, subspaces and mappings in topological spaces. Formalized Mathematics, 1(2):257–261, 1990.

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

[15] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, Berlin, Heidelberg, New York, 1980.

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

[17] Zbigniew Karno. Continuity of mappings over the union of subspaces. Formalized Mathematics, 3(1):1–16, 1992.

[18] Zbigniew Karno. On Kolmogorov topological spaces. Formalized Mathematics, 5(1):119– 124, 1996.

[19] Artur Korniłowicz. Cartesian products of relations and relational structures. Formalized Mathematics, 6(1):145–152, 1997.

[20] Artur Korniłowicz. Definitions and properties of the join and meet of subsets. Formalized Mathematics, 6(1):153–158, 1997.

[21] Artur Korniłowicz. Meet – continuous lattices. Formalized Mathematics, 6(1):159–167, 1997.

[22] Artur Korniłowicz. On the topological properties of meet-continuous lattices. Formalized Mathematics, 6(2):269–277, 1997.

[23] Beata Madras. Irreducible and prime elements. Formalized Mathematics, 6(2):233–239, 1997.

[24] Robert Milewski. Algebraic lattices. Formalized Mathematics, 6(2):249–254, 1997.

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

[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] Alexander Yu. Shibakov and Andrzej Trybulec. The Cantor set. Formalized Mathematics, 5(2):233–236, 1996.

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

[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. Baire spaces, sober spaces. Formalized Mathematics, 6(2):289–294, 1997.

[33] Andrzej Trybulec. Moore-Smith convergence. Formalized Mathematics, 6(2):213–225, 1997.

[34] Andrzej Trybulec. Scott topology. Formalized Mathematics, 6(2):311–319, 1997.

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

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

[37] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

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

446 czesław byliński and piotr rudnicki

[39] Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231–237, 1990.

[40] Mariusz Żynel. The equational characterization of continuous lattices. Formalized Mathematics, 6(2):199–205, 1997.

[41] Mariusz Żynel and Czesław Byliński. Properties of relational structures, posets, lattices and maps. Formalized Mathematics, 6(1):123–130, 1997.

Received August 27, 1997

the scott topology. part ii 447

alalalalalal alalalalalalal

Index of MML Identifiers

ABIAN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 335

ALTCAT 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .329

BIRKHOFF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 389

CLOSURE3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 397

COMSEQ 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .403

EQUATION . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 363

FUNCTOR2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 371

GCD 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 381

GRAPH 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 417

JORDAN4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 351

PSCOMP 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .427

RLVECT 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .411

SUBSTLAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 359

WAYBEL13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 345

WAYBEL14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 441

WELLFND1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 339

YONEDA 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .377

Contents Formaliz. Math. 6 (3)

Basic Properties of Objects and Morphisms

By Beata Madras-Kobus  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 329

Abian’s Fixed Point Theorem

By Piotr Rudnicki and Andrzej Trybulec  . . . . . . . . . . . . . . . . 335

On Same Equivalents of Well-foundedness

By Piotr Rudnicki and Andrzej Trybulec  . . . . . . . . . . . . . . . . 339

Algebraic and Arithmetic Lattices. Part I

By Robert Milewski  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 345

Subsequences of Standard Special Circular Sequences in E_{T}^{2}

By Yatsuka Nakamura et al.  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 351

Lattice of Substitutions

By Adam Grabowski . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 359

Equations in Many Sorted Algebras

By Artur Korniłowicz  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 363

Category of Functors Between Alternative Categories

By Robert Nieszczerzewski  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 371

Yoneda Embedding

By Mirosław Wojciechowski  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 377

The Correctness of the Generic Algorithms of Brown and Henrici

Concerning Addition and Multiplication in Fraction Fields

By Christoph Schwarzweller  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 381

Birkhoff Theorem for Many Sorted Algebras

By Artur Korniłowicz  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 389

Continued on inside back cover

Algebraic Operation on Subsets of Many Sorted Sets

By Agnieszka Julia Marasik  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 397

Convergence and the Limit of Complex Sequences. Serieses

By Yasunari Shidama and Artur Korniłowicz  . . . . . . . . . . . 403

The Steinitz Theorem and the Dimension of a Real Linear Space

By Jing-Chao Chen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 411

Euler Circuits and Paths

By Yatsuka Nakamura and Piotr Rudnicki  . . . . . . . . . . . . . . . 417

Bounding Boxes for Compact Sets in E^{2}

By Czesław Byliński and Piotr Rudnicki  . . . . . . . . . . . . . . . . . 427

The Scott Topology. Part II

By Czesław Byliński and Piotr Rudnicki  . . . . . . . . . . . . . . . . . 441

Index of MML Identifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 448