Preface

As was stated in [3] we publish mathematical papers which are abstracts of Mizar articles to be found in the Main Mizar Library (MML). An article includes certain elements which are transferred to the data base, such as theorems or definitions. This has been due to the fact that the material published there was at first intended to help the Mizar users to handle the data base. Thus the works published there describe the present state of MML and are, in a sense, a report on the expansion of that library. Next to them there are also new mathematical papers because the new method of formalization is not trivial even though it refers to simple mathematical facts.

It must be explained at this point that both the PC-Mizar verifier and MML are being systematically developed. In the case of PC-Mizar it is mainly the Mizar language which is enriched, which makes it more convenient to write articles; the same might be said of proof-checker, which enables one to write shorter proofs and articles.

The development of MML consists in continuous revisions of articles accepted for publication, for instance in the removal of self-evident or repeated theorems (while the numbering of successive theorems in a given article is preserved). We then have the information in a footnote such as ”The proposition (5) has been removed” (see [1], page 450). Previously such a comment was, e.g., ”The proposition (9) was either repeated or obvious” (see [2], page 14).

Please note also that in the articles we use atypical symbolism for the Cartesian product [: :] , and that is no paranthesis in the case of grouping to the left. In the present issue we have changed the format of certain operation. In [4] the functor represented in Mizar by ”∅.X” (the empty set treated as the finite subset of X) was unfortunately TEXed as 0_{X}. Now we corrected this and it is TEXed as ∅_{X}.

Our periodical appears five times a year, which is to say every two months except for the summer holidays period. The present issue, although dated November-December, also includes items contributed after. They have been included because the editors received them before sending the issue 2(5) to the press.

Roman Matuszewski

References

[1] Formalized Mathematics: a computer assisted approach. Volume 2(4), Université Catholique de Louvain, September-October 1991.

[2] Formalized Mathematics: a computer assisted approach. Volume 2(1), Université Catholique de Louvain, January-February 1991.

[3] Andrzej Trybulec. Introduction. Formalized Mathematics, 1(1):7–8, January 1990.

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

616

FORMALIZED MATHEMATICS Vol.2,No.5, November–December 1991 Université Catholique de Louvain

The Topological Space E_{T}^{2}.

Arcs, Line Segments and Special Polygonal Arcs

Agata Darmochwał^{1} Warsaw University Białystok Yatsuka Nakamura Shinshu University

Summary. The notions of arc and line segment are introduced in two-dimensional topological real space E_{T}^{2}. Some basic theorems for these notions are proved. Using line segments, the notion of special polygonal arc is defined. It has been shown that any special polygonal arc is homeomorphic to unit interval . The notion of unit square _{E_{T}^{2}} has been also introduced and some facts about it have been proved.

MML Identifier: TOPREAL1.

The articles [22], [21], [13], [1], [24], [20], [6], [7], [18], [4], [8], [15], [23], [17], [25], [11], [16], [9], [19], [2], [5], [14], [3], [10], and [12] provide the notation and terminology for this paper. In the sequel l_{1} will denote a real number and i, j, n will denote natural numbers. The scheme Fraenkel Alt concerns a non-empty set A, and two unary predicates P and Q, and states that:

{v : P[v] ∨ Q[v]} = {v_{1} : P[v_{1}]} ∪ {v_{2} : Q[v_{2}]}, where v_{2} ranges over elements of A, and v_{1} ranges over elements of A, and v ranges over elements of A for all values of the parameters.

In the sequel d_{1}, d_{2}, d_{3} will be arbitrary. We now state the proposition (2)^{2} ⟨d_{1}, d_{2}, d_{3}⟩ is one-to-one if and only if d_{1} ≠ d_{2} and d_{2} ≠ d_{3} and d_{1} ≠ d_{3}. In the sequel D denotes a non-empty set and p denotes a finite sequence

of elements of D. Let us consider D, p, n. The functor p n yielding a finite sequence of elements of D is defined by: (Def.1) p n = p Seg n.

One can prove the following proposition (3) If n ≤ len p, then len(p n) = n. Let us consider T. A finite sequence of elements of T is a finite sequence of

1The article was written during my work at Shinshu University, 1991.

2The proposition (1) has been removed.

elements of the carrier of T.

We adopt the following convention: p, p_{1}, p_{2}, q, q_{1}, q_{2} will be points of E_{T}^{2} and P, Q, P_{1}, P_{2} will be subsets of E_{T}^{2}. Let us consider p_{1}, p_{2}, P. We say that P is an arc from p_{1} to p_{2} if and only if: (Def.2) P ≠ ∅ and there exists a map f from into (E_{T}^{2}) P such that f is a

homeomorphism and f(0) = p_{1} and f(1) = p_{2}. One can prove the following two propositions:

(4) If P is an arc from p_{1} to p_{2}, then p_{1} ∈ P and p_{2} ∈ P.

(5) If P is an arc from p_{1} to p_{2} and Q is an arc from p_{2} to q_{1} and P ∩ Q = {p_{2}}, then P ∪ Q is an arc from p_{1} to q_{1}.

The subset _{E^{2}} of E_{T}^{2} is defined by the condition (Def.3). (Def.3) _{E^{2}} = {p : p_{1} = 0 ∧ p_{2} ≤ 1 ∧ p_{2} ≥ 0 ∨ p_{1} ≤ 1 ∧ p_{1} ≥ 0 ∧ p_{2} = 1 ∨ p_{1} ≤

1 ∧ p_{1} ≥ 0 ∧ p_{2} = 0 ∨ p_{1} = 1 ∧ p_{2} ≤ 1 ∧ p_{2} ≥ 0}. Let us consider p_{1}, p_{2}. The functor L(p_{1}, p_{2}) yielding a non-empty subset of

E_{T}^{2} is defined as follows: (Def.4) L(p_{1}, p_{2}) = {p : ⋁_{l_{1}}[0 ≤ l_{1} ∧ l_{1} ≤ 1 ∧ p = (1 − l_{1}) · p_{1} + l_{1} · p_{2}]}.

Next we state a number of propositions:

(6) p_{1} ∈ L(p_{1}, p_{2}) and p_{2} ∈ L(p_{1}, p_{2}).

(7) L(p, p) = {p}.

(8) L(p_{1}, p_{2}) = L(p_{2}, p_{1}).

(9) If p_{1}_{1} ≤ p_{2}_{1} and p ∈ L(p_{1}, p_{2}), then p_{1}_{1} ≤ p_{1} and p_{1} ≤ p_{2}_{1}.

(10) If p_{1}_{2} ≤ p_{2}_{2} and p ∈ L(p_{1}, p_{2}), then p_{1}_{2} ≤ p_{2} and p_{2} ≤ p_{2}_{2}.

(11) If p ∈ L(p_{1}, p_{2}), then L(p_{1}, p_{2}) = L(p_{1}, p) ∪ L(p, p_{2}).

(12) If q_{1} ∈ L(p_{1}, p_{2}) and q_{2} ∈ L(p_{1}, p_{2}), then L(q_{1}, q_{2}) ⊆ L(p_{1}, p_{2}).

(13) If p ∈ L(p_{1}, p_{2}) and q ∈ L(p_{1}, p_{2}), then L(p_{1}, p_{2}) = L(p_{1}, p) ∪ L(p, q) ∪ L(q, p_{2}).

(14) If p ∈ L(p_{1}, p_{2}), then L(p_{1}, p) ∩ L(p, p_{2}) = {p}.

(15) If p_{1} ≠ p_{2}, then L(p_{1}, p_{2}) is an arc from p_{1} to p_{2}.

(16) If P is an arc from p_{1} to p_{2} and P ∩ L(p_{2}, q_{1}) = {p_{2}}, then P ∪ L(p_{2}, q_{1}) is an arc from p_{1} to q_{1}.

(17) If P is an arc from p_{2} to p_{1} and L(q_{1}, p_{2}) ∩ P = {p_{2}}, then L(q_{1}, p_{2}) ∪ P is an arc from q_{1} to p_{1}.

(18) If p_{1} ≠ p_{2} or p_{2} ≠ q_{1} but L(p_{1}, p_{2}) ∩ L(p_{2}, q_{1}) = {p_{2}}, then L(p_{1}, p_{2}) ∪ L(p_{2}, q_{1}) is an arc from p_{1} to q_{1}.

(19) (i) L([0, 0], [0, 1]) = {p_{1} : p_{1}_{1} = 0 ∧ p_{1}_{2} ≤ 1 ∧ p_{1}_{2} ≥ 0}, (ii) L([0, 1], [1, 1]) = {p_{2} : p_{2}_{1} ≤ 1 ∧ p_{2}_{1} ≥ 0 ∧ p_{2}_{2} = 1}, (iii) L([0, 0], [1, 0]) = {q_{1} : q_{1}_{1} ≤ 1 ∧ q_{1}_{1} ≥ 0 ∧ q_{1}_{2} = 0}, (iv) L([1, 0], [1, 1]) = {q_{2} : q_{2}_{1} = 1 ∧ q_{2}_{2} ≤ 1 ∧ q_{2}_{2} ≥ 0}.

the topological space E_{t}^{2}…. 619

(20) _{E^{2}} = L([0, 0], [0, 1]) ∪ L([0, 1], [1, 1]) ∪ (L([0, 0], [1, 0]) ∪ L([1, 0], [1, 1])).

(21) L([0, 0], [0, 1]) ∩ L([0, 1], [1, 1]) = {[0, 1]}.

(22) L([0, 0], [1, 0]) ∩ L([1, 0], [1, 1]) = {[1, 0]}.

(23) L([0, 0], [0, 1]) ∩ L([0, 0], [1, 0]) = {[0, 0]}.

(24) L([0, 1], [1, 1]) ∩ L([1, 0], [1, 1]) = {[1, 1]}.

(25) L([0, 0], [1, 0]) ∩ L([0, 1], [1, 1]) = ∅.

(26) L([0, 0], [0, 1]) ∩ L([1, 0], [1, 1]) = ∅.

In the sequel f, f_{1}, f_{2}, h will be finite sequences of elements of E_{T}^{2}. Let us consider f, i, j. The functor L(f, i, j) yielding a subset of E_{T}^{2} is defined as follows: (Def.5) (i) for all p_{1}, p_{2} such that p_{1} = f(i) and p_{2} = f(j) holds L(f, i, j) =

L(p_{1}, p_{2}) if i ∈ Seg len f and j ∈ Seg len f, (ii) L(f, i, j) = ∅, otherwise.

The following proposition is true

(27) If i ∈ Seg len f and j ∈ Seg len f, then f(i) ∈ L(f, i, j) and f(j) ∈

L(f, i, j). Let us consider f. The functor L̃(f) yields a subset of E_{T}^{2} and is defined as

follows: (Def.6) L̃(f) = ⋃{L(f, i, i + 1) : 1 ≤ i ∧ i ≤ len f − 1}.

One can prove the following propositions:

(28) len f = 0 or len f = 1 if and only if L̃(f) = ∅.

(29) If len f ≥ 2, then L̃(f) ≠ ∅.

Let us consider f. We say that f is a special sequence if and only if the conditions (Def.7) is satisfied. (Def.7) (i) f is one-to-one,

(ii) len f ≥ 3, (iii) for every i such that 1 ≤ i and i ≤ len f −2 holds L(f, i, i+1)∩L(f, i+

1, i + 2) = {f(i + 1)}, (iv) for all i, j such that i−j > 1 or j −i > 1 holds L(f, i, i+1)∩L(f, j, j +

1) = ∅,

(v) for all i, p_{1}, p_{2} such that 1 ≤ i and i ≤ len f − 1 and p_{1} = f(i) and p_{2} = f(i + 1) holds p_{1}_{1} = p_{2}_{1} or p_{1}_{2} = p_{2}_{2}.

The following propositions are true:

(30) There exist f_{1}, f_{2} such that f_{1} is a special sequence and f_{2} is a special sequence and _{E^{2}} = L̃(f_{1}) ∪ L̃(f_{2}) and L̃(f_{1}) ∩ L̃(f_{2}) = {[0, 0], [1, 1]} and f_{1}(1) = [0, 0] and f_{1}(len f_{1}) = [1, 1] and f_{2}(1) = [0, 0] and f_{2}(len f_{2}) = [1, 1].

(31) If h is a special sequence and P = L̃(h), then for all p_{1}, p_{2} such that

p_{1} = h(1) and p_{2} = h(len h) holds P is an arc from p_{1} to p_{2}. Let us consider P. We say that P is a special polygonal arc if and only if:

(Def.8) there exists f such that f is a special sequence and P = L̃(f).

620 agata darmochwał and yatsuka nakamura

The following propositions are true:

(32) If P is a special polygonal arc, then P ≠ ∅.

(33) If f is a special sequence, then L̃(f) is a special polygonal arc.

(34) There exist P_{1}, P_{2} such that P_{1} is a special polygonal arc and P_{2} is a special polygonal arc and _{E^{2}} = P_{1} ∪ P_{2} and P_{1} ∩ P_{2} = {[0, 0], [1, 1]}.

(35) If P is a special polygonal arc, then there exist p_{1}, p_{2} such that P is an arc from p_{1} to p_{2}.

(36) If P is a special polygonal arc, then there exists a map f from into (E_{T}^{2}) P such that f is a homeomorphism.

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] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481– 485, 1991.

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

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

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

[7] Czesław Byliński. 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] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383–386, 1990.

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

[11] Agata Darmochwał. Families of subsets, subspaces and mappings in topological spaces. Formalized Mathematics, 1(2):257–261, 1990.

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

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

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

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

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

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

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

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

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

[21] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

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

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

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

the topological space E_{t}^{2}…. 621

[25] Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized

Mathematics, 1(1):231–237, 1990.

Received November 21, 1991 622

Cyclic Groups and Some of Their Properties - Part I

Dariusz Surowik Warsaw University Białystok

Summary. Some properties of finite groups are proved. The notion of cyclic group is defined next, some cyclic groups are given, for example the group of integers with addition operations. Chosen properties of cyclic groups are proved next.

MML Identifier: GR CY 1.

The articles [19], [7], [12], [8], [13], [2], [3], [16], [6], [5], [18], [1], [11], [4], [15], [28], [17], [21], [14], [23], [27], [22], [25], [26], [24], [20], [10], and [9] provide the notation and terminology for this paper. For simplicity we adopt the following rules: i_{1} denotes an element of , j_{1} denotes an integer, p, s, k, n, l, m denote natural numbers, x is arbitrary, G denotes a group, a, b denote elements of G, and I denotes a finite sequence of elements of . We now state several propositions:

(1) For every n such that n > 0 holds m mod n = (n · k + m) mod n.

(2) For every n such that n > 0 holds (p+s)modn = ((pmodn)+s)modn.

(3) For every n such that n > 0 holds (p+s)modn = (p+(smodn))modn.

(4) For every k such that k < n holds k mod n = k.

(5) For every n such that n > 0 holds n mod n = 0.

(6) For every n such that n > 0 holds 0 = 0 mod n.

(7) If k + l = m, then l ≤ m.

(8) For all k, l, m such that l = m and m = k + l holds k = 0.

Let us consider n satisfying the condition: n > 0. The functor _{n} yields a non-empty subset of and is defined by: (Def.1) _{n} = {p : p < n}.

We now state several propositions:

(9) For every n such that n > 0 holds if x ∈ _{n}, then x is a natural number.

(10) For every n such that n > 0 holds s ∈ _{n} if and only if s < n.

(11) For every n such that n > 0 holds _{n} ⊆ .

(12) For every n such that n > 0 holds 0 ∈ _{n}.

(13) _{1} = {0}.

The binary operation +_{}on is defined by: (Def.2) for all elements i_{1}, i_{2} of holds (+_{})(i_{1}, i_{2}) = +_{}(i_{1}, i_{2}).

The following propositions are true:

(14) For all integers i_{1}, i_{2} holds (+_{})(i_{1}, i_{2}) = i_{1} + i_{2}.

(15) For every i_{1} such that i_{1} = 0 holds i_{1} is a unity w.r.t. +_{}.

(16) 1_{+_{}}= 0.

(17) +_{}has a unity.

(18) +_{}is commutative.

(19) +_{}is associative.

Let F be a finite sequence of elements of . The functor ∑ F yields an integer and is defined by: (Def.3) ∑ F = +_{}F.

Next we state several propositions:

(20) ∑(I ^{}⟨i_{1}⟩) = ∑ I +^{@}i_{1}.

(21) ∑⟨i_{1}⟩ = i_{1}.

(22) ∑(ε_{}) = 0.

(23) For all non-empty sets D, D_{1} holds ε_{D} = ε_{D_{1}}.

(24) For every finite sequence I of elements of holds ∏((len I ⟼ a)^{I}) =

a^{∑ I}. Let G be a group, and let a be an element of G. Then {a} is a subset of G. We now state several propositions:

(25) b ∈ gr({a}) if and only if there exists j_{1} such that b = a^{j_{1}}.

(26) If G is finite, then a is not of order 0.

(27) If G is finite, then ord(a) = ord(gr({a})).

(28) If G is finite, then ord(a) | ord(G).

(29) If G is finite, then a^{ord(G)} = 1_{G}.

(30) If G is finite, then (a^{n})^{−1} = a^{ord(G)−(n mod ord(G))}.

(31) For every strict group G such that ord(G) > 1 there exists an element a of G such that a ≠ 1_{G}.

(32) For every strict group G such that G is finite and ord(G) = p and p is prime and for every strict subgroup H of G holds H = {1}_{G} or H = G.

(33) ⟨ , +_{}⟩ is a group.

The group ^{+} is defined as follows: (Def.4) ^{+} = ⟨ , +_{}⟩.

Let D be a non-empty set, and let D_{1} be a non-empty subset of D, and let D_{2} be a non-empty subset of D_{1}. We see that the element of D_{2} is an element of D_{1}.

Let us consider n satisfying the condition: n > 0. The functor +_{n} yielding a binary operation on _{n} is defined by: (Def.5) for all elements k, l of _{n} holds +_{n}(k, l) = (k + l) mod n.

Next we state the proposition

(34) For every n such that n > 0 holds ⟨ _{n}, +_{n}⟩ is a group.

Let us consider n satisfying the condition: n > 0. The functor _{n}^{+} yields a strict group and is defined by: (Def.6) _{n}^{+} = ⟨ _{n}, +_{n}⟩.

Next we state two propositions:

(35) 1_{^{+}} = 0.

(36) For every n such that n > 0 holds 1_{_{n}^{+}} = 0.

Let h be an element of ^{+}. The functor ^{@}h yields an integer and is defined as follows: (Def.7) ^{@}h = h.

Let h be an integer. The functor ^{@}h yielding an element of ^{+} is defined as follows: (Def.8) ^{@}h = h.

The following proposition is true

(37) For every element h of ^{+} holds h^{−1} = −^{@}h.

In the sequel G_{1} will denote a subgroup of ^{+} and h will denote an element of ^{+}. Next we state two propositions:

(38) For every h such that h = 1 and for every k holds h^{k} = k.

(39) For all h, j_{1} such that h = 1 holds j_{1} = h^{j_{1}}.

A strict group is said to be a cyclic group if: (Def.9) there exists an element a of it such that it = gr({a}).

One can prove the following propositions:

(40) {1}_{G} is a cyclic group.

(41) For every strict group G holds G is a cyclic group if and only if there exists an element a of G such that for every element b of G there exists j_{1} such that b = a^{j_{1}}.

(42) For every strict group G such that G is finite holds G is a cyclic group if and only if there exists an element a of G such that for every element b of G there exists n such that b = a^{n}.

(43) For every strict group G such that G is finite holds G is a cyclic group if and only if there exists an element a of G such that ord(a) = ord(G).

(44) For every strict subgroup H of G such that G is finite and G is a cyclic group and H is a subgroup of G holds H is a cyclic group.

626 dariusz surowik

(45) For every strict group G such that G is finite and ord(G) = p and p is prime holds G is a cyclic group.

(46) For every n such that n > 0 there exists an element g of _{n}^{+} such that for every element b of _{n}^{+} there exists j_{1} such that b = g^{j_{1}}.

(47) If G is a cyclic group, then G is an Abelian group.

(48) ^{+} is a cyclic group.

(49) For every n such that n > 0 holds _{n}^{+} is a cyclic group.

(50) ^{+} is an Abelian group.

(51) For every n such that n > 0 holds _{n}^{+} is an Abelian group.

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. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[5] Czesław Byliński. Binary operations applied to finite sequences. Formalized Mathematics, 1(4):643–649, 1990.

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

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

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

[9] Czesław Byliński. Semigroup operations on finite subsets. Formalized Mathematics, 1(4):651–656, 1990.

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

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

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

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

[14] Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relative primes. Formalized Mathematics, 1(5):829–832, 1990.

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

[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. Semilattice operations on finite subsets. Formalized Mathematics, 1(2):369–376, 1990.

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

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

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

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

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

cyclic groups and some of their properties - … 627

[24] Wojciech A. Trybulec. Lattice of subgroups of a group. Frattini subgroup. Formalized Mathematics, 2(1):41–47, 1991.

[25] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569–573, 1990.

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

[27] Wojciech A. Trybulec. Subgroup and cosets of subgroups. Formalized Mathematics, 1(5):855–864, 1990.

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

628

Isomorphisms of Categories

Andrzej Trybulec Warsaw University Białystok

Summary. We continue the development of the category theory basically following [12] (compare also [11]). We define the concept of isomorphic categories and prove basic facts related, e.g. that the Cartesian product of categories is associative up to the isomorphism. We introduce the composition of a functor and a transformation, and of transformation and a functor, and afterwards we define again those concepts for natural transformations. Let us observe, that we have to duplicate those concepts because of the permissiveness: if a functor F is not naturally transformable to G, then natural transformation from F to G has no fixed meaning, hence we cannot claim that the composition of it with a functor as a transformation results in a natural transformation. We define also the so called horizontal composition of transformations ([12], p.140, exercise 4.2,5(C)) and prove interchange law ([11], p.44). We conclude with the definition of equivalent categories.

MML Identifier: ISOCAT 1.

The articles [16], [17], [4], [5], [3], [7], [1], [2], [10], [13], [8], [14], [6], [9], and [15] provide the notation and terminology for this paper. We adopt the following convention: A, B, C, D will denote categories, F, F_{1}, F_{2} will denote functors from A to B, and G will denote a functor from B to C. One can prove the following propositions:

(1) For all functions F, G such that F is one-to-one and G is one-to-one holds [: F, G:] is one-to-one.

(2) rng π_{1}(A × B) = the morphisms of A and rng π_{2}(B × A) = the morphisms of A.

(3) For every morphism f of A such that f is invertible holds F (f) is invertible.

(4) For every functor F from A to B and for every functor G from B to A holds F · id_{A} = F and id_{A} · G = G.

(5) For all objects a, b of A such that hom(a, b) ≠ ∅ and for every morphism f from a to b and for every functor F from A to B and for every functor G from B to C holds (G · F)(f) = G(F (f)).

(6) For all objects a, b, c of A such that hom(a, b) ≠ ∅ and hom(b, c) ≠ ∅ and for every morphism f from a to b and for every morphism g from b to c and for every functor F from A to B holds F (g · f) = F (g) · F (f).

(7) For all functors F_{1}, F_{2} from A to B such that F_{1} is transformable to F_{2} and for every transformation t from F_{1} to F_{2} and for every object a of A holds t(a) ∈ hom(F_{1}(a), F_{2}(a)).

(8) For all functors F_{1}, F_{2} from A to B and for all functors G_{1}, G_{2} from B to C such that F_{1} is transformable to F_{2} and G_{1} is transformable to G_{2} holds G_{1} · F_{1} is transformable to G_{2} · F_{2}.

(9) For all functors F_{1}, F_{2} from A to B such that F_{1} is transformable to F_{2} and for every transformation t from F_{1} to F_{2} such that t is invertible and for every object a of A holds F_{1}(a) and F_{2}(a) are isomorphic.

Let us consider C, D. Let us observe that the mode below can be characterized by another conditions, which are equivalent to the formulas previously defining them. In accordance the mode Let us note that one can characterize the mode functor from C to D, by the following (equivalent) condition: (Def.1) (i) for every object c of C there exists an object d of D such that

it(id_{c}) = id_{d}, (ii) for every morphism f of C holds it(id_{dom f}) = id_{dom it(f)} and it(id_{cod f}) =

id_{cod it(f)}, (iii) for all morphisms f, g of C such that dom g = cod f holds it(g · f) =

it(g) · it(f).

Let us consider A. Then id_{A} is a functor from A to A. Let us consider B, C, and let F be a functor from A to B, and let G be a functor from B to C. Then G · F is a functor from A to C.

In the sequel o, m are arbitrary. We now state three propositions:

(10) If F is an isomorphism, then for every morphism g of B there exists a morphism f of A such that F (f) = g.

(11) If F is an isomorphism, then for every object b of B there exists an object a of A such that F (a) = b.

(12) If F is one-to-one, then Obj F is one-to-one.

Let us consider A, B, F. Let us assume that F is an isomorphism. The functor F^{−1} yields a functor from B to A and is defined by: (Def.2) F^{−1} = F^{−1}.

Let us consider A, B, F. Let us note that one can characterize the predicate F is an isomorphism by the following (equivalent) condition: (Def.3) F is one-to-one and rng F = the morphisms of B.

Next we state several propositions:

(13) If F is an isomorphism, then F^{−1} is an isomorphism.

(14) If F is an isomorphism, then (Obj F)^{−1} = Obj(F^{−1}).

(15) If F is an isomorphism, then (F^{−1})^{−1} = F.

(16) If F is an isomorphism, then F · F^{−1} = id_{B} and F^{−1} · F = id_{A}.

(17) If F is an isomorphism and G is an isomorphism, then G · F is an

isomorphism. In the sequel t_{1} denotes a natural transformation from F_{1} to F_{2} and t_{2} denotes

a natural transformation from F to F_{2}. We now define two new predicates. Let us consider A, B. We say that A and B are isomorphic if and only if: (Def.4) there exists a functor F from A to B such that F is an isomorphism. We write A ≅ B if A and B are isomorphic.

The following propositions are true:

(18) A ≅ A.

(19) If A ≅ B, then B ≅ A.

(20) If A ≅ B and B ≅ C, then A ≅ C.

(21) [: ˙ (o, m), A:] ≅ A.

(22) [: A, B:] ≅ [: B, A:].

(23) [: [: A, B:], C:] ≅ [: A, [: B, C:] :].

(24) If A ≅ B and C ≅ D, then [: A, C:] ≅ [: B, D:].

Let us consider A, B, C, and let F_{1}, F_{2} be functors from A to B satisfying the condition: F_{1} is transformable to F_{2}. Let t be a transformation from F_{1} to F_{2}, and let G be a functor from B to C. The functor G·t yields a transformation from G · F_{1} to G · F_{2} and is defined as follows: (Def.5) G · t = G · t.

Let us consider A, B, C, and let G_{1}, G_{2} be functors from B to C satisfying the condition: G_{1} is transformable to G_{2}. Let F be a functor from A to B, and let t be a transformation from G_{1} to G_{2}. The functor t · F yielding a transformation from G_{1} · F to G_{2} · F is defined by: (Def.6) t · F = t · Obj F.

We now state three propositions:

(25) For all functors G_{1}, G_{2} from B to C such that G_{1} is transformable to G_{2} and for every functor F from A to B and for every transformation t from G_{1} to G_{2} and for every object a of A holds (t · F)(a) = t(F (a)).

(26) For all functors F_{1}, F_{2} from A to B such that F_{1} is transformable to F_{2} and for every transformation t from F_{1} to F_{2} and for every functor G from B to C and for every object a of A holds (G · t)(a) = G(t(a)).

(27) For all functors F_{1}, F_{2} from A to B and for all functors G_{1}, G_{2} from B to C such that F_{1} is naturally transformable to F_{2} and G_{1} is naturally transformable to G_{2} holds G_{1} · F_{1} is naturally transformable to G_{2} · F_{2}.

Let us consider A, B, C, and let F_{1}, F_{2} be functors from A to B satisfying the condition: F_{1} is naturally transformable to F_{2}. Let t be a natural transformation from F_{1} to F_{2}, and let G be a functor from B to C. The functor G · t yielding a natural transformation from G · F_{1} to G · F_{2} is defined by:

(Def.7) G · t = G · t.

Next we state the proposition

(28) For all functors F_{1}, F_{2} from A to B such that F_{1} is naturally transformable to F_{2} and for every natural transformation t from F_{1} to F_{2} and for every functor G from B to C and for every object a of A holds (G · t)(a) = G(t(a)).

Let us consider A, B, C, and let G_{1}, G_{2} be functors from B to C satisfying the condition: G_{1} is naturally transformable to G_{2}. Let F be a functor from A to B, and let t be a natural transformation from G_{1} to G_{2}. The functor t · F yields a natural transformation from G_{1} · F to G_{2} · F and is defined as follows:

(Def.8) t · F = t · F.

The following proposition is true

(29) For all functors G_{1}, G_{2} from B to C such that G_{1} is naturally transformable to G_{2} and for every functor F from A to B and for every natural transformation t from G_{1} to G_{2} and for every object a of A holds (t · F)(a) = t(F (a)).

For simplicity we follow the rules: F, F_{1}, F_{2}, F_{3} are functors from A to B, G, G_{1}, G_{2}, G_{3} are functors from B to C, H, H_{1}, H_{2} are functors from C to D, s is a natural transformation from F_{1} to F_{2}, s′ is a natural transformation from F_{2} to F_{3}, t is a natural transformation from G_{1} to G_{2}, t′ is a natural transformation from G_{2} to G_{3}, and u is a natural transformation from H_{1} to H_{2}. We now state a number of propositions:

(30) If F_{1} is naturally transformable to F_{2}, then for every object a of A holds hom(F_{1}(a), F_{2}(a)) ≠ ∅.

(31) If F_{1} is naturally transformable to F_{2}, then for all natural transformations t_{1}, t_{2} from F_{1} to F_{2} such that for every object a of A holds t_{1}(a) = t_{2}(a) holds t_{1} = t_{2}.

(32) If F_{1} is naturally transformable to F_{2} and F_{2} is naturally transformable to F_{3}, then G · (s′ ^{∘} s) = G · s′ ^{∘} G · s.

(33) If G_{1} is naturally transformable to G_{2} and G_{2} is naturally transformable to G_{3}, then (t′ ^{∘} t) · F = t′ · F ^{∘} t · F.

(34) If H_{1} is naturally transformable to H_{2}, then (u · G) · F = u · (G · F).

(35) If G_{1} is naturally transformable to G_{2}, then (H · t) · F = H · (t · F).

(36) If F_{1} is naturally transformable to F_{2}, then (H · G) · s = H · (G · s).

(37) id_{G} · F = id_{(G·F)}.

(38) G · id_{F} = id_{(G·F)}.

(39) If G_{1} is naturally transformable to G_{2}, then t · id_{B} = t.

(40) If F_{1} is naturally transformable to F_{2}, then id_{B} · s = s.

Let us consider A, B, C, F_{1}, F_{2}, G_{1}, G_{2}, s, t. The functor t s yields a natural transformation from G_{1} · F_{1} to G_{2} · F_{2} and is defined as follows: (Def.9) t s = t · F_{2} ^{∘} G_{1} · s.

We now state several propositions:

(41) If F_{1} is naturally transformable to F_{2} and G_{1} is naturally transformable to G_{2}, then t s = G_{2} · s^{∘} t · F_{1}.

(42) If F_{1} is naturally transformable to F_{2}, then id_{(id_{B})} s = s.

(43) If G_{1} is naturally transformable to G_{2}, then t id_{(id_{B})} = t.

(44) If F_{1} is naturally transformable to F_{2} and G_{1} is naturally transformable to G_{2} and H_{1} is naturally transformable to H_{2}, then u (t s) = (u t) s.

(45) If G_{1} is naturally transformable to G_{2}, then t · F = t id_{F}.

(46) If F_{1} is naturally transformable to F_{2}, then G · s = id_{G} s.

(47) If F_{1} is naturally transformable to F_{2} and F_{2} is naturally transformable to F_{3} and G_{1} is naturally transformable to G_{2} and G_{2} is naturally transformable to G_{3}, then (t′ ^{∘} t) (s′ ^{∘} s) = t′ s′ ^{∘} t s.

(48) For every functor F from A to B and for every functor G from C to D and for all functors I, J from B to C such that I ≅ J holds G · I ≅ G · J and I · F ≅ J · F.

(49) For every functor F from A to B and for every functor G from B to A and for every functor I from A to A such that I ≅ id_{A} holds F · I ≅ F and I · G ≅ G.

We now define two new predicates. Let A, B be categories. We say that A is equivalent with B if and only if:

(Def.10) there exists a functor F from A to B and there exists a functor G from

B to A such that G · F ≅ id_{A} and F · G ≅ id_{B}. A and B are equivalent stands for A is equivalent with B.

We now state four propositions:

(50) If A ≅ B, then A is equivalent with B.

(51) A is equivalent with A.

(52) If A and B are equivalent, then B and A are equivalent.

(53) If A and B are equivalent and B and C are equivalent, then A and C

are equivalent. Let us consider A, B. Let us assume that A and B are equivalent. A functor

from A to B is called an equivalence of A and B if: (Def.11) there exists a functor G from B to A such that G · it ≅ id_{A} and it · G ≅

id_{B}. Next we state several propositions:

(54) id_{A} is an equivalence of A and A.

(55) If A and B are equivalent and B and C are equivalent, then for every equivalence F of A and B and for every equivalence G of B and C holds G · F is an equivalence of A and C.

634 andrzej trybulec

(56) If A and B are equivalent, then for every equivalence F of A and B there exists an equivalence G of B and A such that G · F ≅ id_{A} and F · G ≅ id_{B}.

(57) For every functor F from A to B and for every functor G from B to A such that G · F ≅ id_{A} holds F is faithful.

(58) If A and B are equivalent, then for every equivalence F of A and B holds F is full and F is faithful and for every object b of B there exists an object a of A such that b and F (a) are isomorphic.

References

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

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

[3] Czesław Byliński. Basic functions and operations on functions. Formalized Mathematics, 1(1):245–254, 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] Czesław Byliński. Introduction to categories and functors. Formalized Mathematics, 1(2):409–420, 1990.

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

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

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

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

[11] Saunders Mac Lane. Categories for the Working Mathematician. Volume 5 of Graduate Texts in Mathemaics, Springer Verlag, New York, Heidelberg, Berlin, 1971.

[12] Zbigniew Semadeni and Antoni Wiweger. Wstȩp do teorii kategorii i funktorów. Volume 45 of Biblioteka Matematyczna, PWN, Warszawa, 1978.

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

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

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

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

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

Similarity of Formulae

Agata Darmochwał Warsaw University Andrzej Trybulec Warsaw University Białystok

Summary. The main objective of the paper is to define the concept of the similarity of formulas. We mean by similar formulas the two formulas that differs only in the names of bound variables. Some authors (compare [16]) call such formulas congruent. We use the word similar following [14,12,15]. The concept is unjustfully neglected in many logical handbooks. It is intuitively quite clear, however the exact definition is not simple. As far as we know, only W.A.Pogorzelski and T.Prucnal

[15] define it in the precise way. We follow basically the Pogorzelski’s definition (compare [14]). We define renumaration of bound variables and we say that two formulas are similar if after renumaration are equal. Therefore we need a rule of chosing bound variables independent of the original choice. Quite obvious solution is to use consecutively variables x_{k+1}, x_{k+2},…, where k is the maximal index of free variable occurring in the formula. Therefore after the renumaration we get the new formula in which different quantifiers bind different variables. It is the reason that the result of renumaration applied to a formula φ we call φ with variables separated.

MML Identifier: CQC SIM1.

The notation and terminology used in this paper are introduced in the following articles: [23], [27], [20], [24], [19], [13], [5], [6], [18], [3], [10], [26], [21], [11], [2], [25], [22], [8], [17], [1], [9], [4], and [7]. One can prove the following four propositions:

(1) For arbitrary x, y and for every function f holds (f +· ({x} ⟼ y))^{∘} {x} = {y}.

(2) For all sets K, L and for arbitrary x, y and for every function f holds (f +· (L ⟼ y))^{∘} K ⊆ f ^{∘} K ∪ {y}.

(3) For arbitrary x, y and for every function g and for every set A holds (g +· ({x} ⟼ y))^{∘} (A \ {x}) = g^{∘} (A \ {x}).

(4) For arbitrary x, y and for every function g and for every set A such that y ∉ g^{∘} (A \ {x}) holds (g +· ({x} ⟼ y))^{∘} (A \ {x}) = (g +· ({x} ⟼ y))^{∘} A \ {y}.

For simplicity we follow the rules: p, q, r, s denote elements of CQC-WFF , x denotes an element of BoundVar , i, k, l, m, n denote elements of , l_{1} denotes a variables list of k, and P denotes a k-ary predicate symbol. The following propositions are true:

(5) If p is atomic, then there exist k, P, l_{1} such that p = P [l_{1}].

(6) If p is negative, then there exists q such that p = ¬q.

(7) If p is conjunctive, then there exist q, r such that p = q ∧ r.

(8) If p is universal, then there exist x, q such that p = ∀_{x}q.

(9) For every non-empty set D and for every finite sequence l of elements of D holds rng l = {l(i) : 1 ≤ i ∧ i ≤ len l}.

In this article we present several logical schemes. The scheme NUBFuncExD deals with a non-empty set A, a non-empty set B, and a binary predicate P, and states that:

there exists a function f from A into B such that for every element e of A holds P[e, f(e)] provided the parameters satisfy the following condition:

• for every element e of A there exists an element u of B such that P[e, u].

The scheme NUBFuncEx2D deals with a non-empty set A, a non-empty set B, a non-empty set C, and a ternary predicate P, and states that:

there exists a function f from [: A, B:] into C such that for every element x of A and for every element y of B holds P[x, y, f(⟨⟨x, y⟩⟩)] provided the parameters meet the following condition:

• for every element x of A and for every element y of B there exists an element u of C such that P[x, y, u].

The scheme QC Func ExN deals with a non-empty set A, an element B of A, a unary functor F yielding an element of A, a binary functor G yielding an element of A, a ternary functor H yielding an element of A, and a binary functor I yielding an element of A and states that:

there exists a function F from WFF into A such that for every element p of WFF and for all elements d_{1}, d_{2} of A holds if p = VERUM, then F (p) = B but if p is atomic, then F (p) = F(p) but if p is negative and d_{1} = F (Arg(p)), then F (p) = G(d_{1}, p) but if p is conjunctive and d_{1} = F (LeftArg(p)) and d_{2} = F (RightArg(p)), then F (p) = H(d_{1}, d_{2}, p) but if p is universal and d_{1} = F (Scope(p)), then F (p) = I(d_{1}, p) for all values of the parameters.

The scheme CQCF2 Func Ex deals with a non-empty set A, a non-empty set B, an element C of B^{A}, a ternary functor F yielding an element of B^{A}, a binary functor G yielding an element of B^{A}, a 4-ary functor H yielding an element of B^{A}, and a ternary functor I yielding an element of B^{A} and states that:

there exists a function F from CQC-WFF into B^{A} such that F (VERUM) = C and for every k and for every variables list l of k and for every k-ary predicate symbol P holds F (P [l]) = F(k, P, l) and for all r, s, x and for all functions f, g from A into B such that f = F (r) and g = F (s) holds F (¬r) = G(f, r) and F (r ∧ s) = H(f, g, r, s) and F (∀_{x}r) = I(x, f, r) for all values of the parameters.

The scheme CQCF2 FUniq concerns a non-empty set A, a non-empty set B, a function C from CQC-WFF into B^{A}, a function D from CQC-WFF into B^{A}, a function E from A into B, a ternary functor F yielding a function from A into B, a binary functor G yielding a function from A into B, a 4-ary functor H yielding a function from A into B, and a ternary functor I yielding a function from A into B and states that:

C = D provided the parameters meet the following requirements:

• C(VERUM) = E,

• for all k, l_{1}, P holds C(P [l_{1}]) = F(k, P, l_{1}),

• Given r, s, x. Then for all functions f, g from A into B such that f = C(r) and g = C(s) holds C(¬r) = G(f, r) and C(r ∧ s) = H(f, g, r, s) and C(∀_{x}r) = I(x, f, r),

• D(VERUM) = E,

• for all k, l_{1}, P holds D(P [l_{1}]) = F(k, P, l_{1}),

• Given r, s, x. Then for all functions f, g from A into B such that f = D(r) and g = D(s) holds D(¬r) = G(f, r) and D(r ∧ s) = H(f, g, r, s) and D(∀_{x}r) = I(x, f, r).

We now state four propositions:

(10) p is a subformula of ¬p.

(11) p is a subformula of p ∧ q and q is a subformula of p ∧ q.

(12) p is a subformula of ∀_{x}p.

(13) For every variables list l of k and for every i such that 1 ≤ i and i ≤ len l

holds l(i) ∈ BoundVar. Let D be a non-empty set, and let f be a function from D into CQC-WFF .

The functor NEG(f) yielding an element of CQC-WFF^{D} is defined as follows: (Def.1) for every element a of D and for every element p of CQC-WFF such

that p = f(a) holds (NEG(f))(a) = ¬p. In the sequel f, h will denote elements of BoundVar^{BoundVar} and K will

denote a finite subset of BoundVar . Let f, g be functions from

[: , BoundVar^{BoundVar} :] into CQC-WFF , and let n be a natural number. The functor CON(f, g, n) yields an element of CQC-WFF^{[: , BoundVar^{BoundVar} :]} and is defined by: (Def.2) for all k, h, p, q such that p = f(⟨⟨k, h⟩⟩) and q = g(⟨⟨k + n, h⟩⟩) holds

(CON(f, g, n))(⟨⟨k, h⟩⟩) = p ∧ q. Let f be a function from [: , BoundVar^{BoundVar} :] into CQC-WFF , and

let x be a bound variable. The functor UNIV(x, f) yielding an element of CQC-WFF^{[: , BoundVar^{BoundVar} :]} is defined by:

(Def.3) for all k, h, p such that p = f(⟨⟨k + 1, h +· ({x} ⟼ x_{k})⟩⟩) holds (UNIV(x, f))(⟨⟨k, h⟩⟩) = ∀_{x_{k}}p.

Let us consider k, and let l be a variables list of k, and let f be an element of BoundVar^{BoundVar} . Then f · l is a variables list of k.

Let us consider k, and let P be a k-ary predicate symbol, and let l be a variables list of k. The functor ATOM(P, l) yields an element of

CQC-WFF^{[: , BoundVar^{BoundVar} :]}

and is defined as follows: (Def.4) for all n, h holds (ATOM(P, l))(⟨⟨n, h⟩⟩) = P [h · l].

Let us consider p. The number of quantifiers in p yields an element of and is defined by the condition (Def.5). (Def.5) There exists a function F from CQC-WFF into such that the number

of quantifiers in p = F (p) and for all r, s, x, k and for every variables list l of k and for every k-ary predicate symbol P and for all elements r′, s′ of such that r′ = F (r) and s′ = F (s) holds F (VERUM) = 0 and F (P [l]) = 0 and F (¬r) = r′ and F (r ∧ s) = r′ + s′ and F (∀_{x}r) = r′ + 1.

Let f be a function from CQC-WFF into CQC-WFF^{[: , BoundVar^{BoundVar} :]} , and let x be an element of CQC-WFF . Then f(x) is an element of CQC-WFF^{[: , BoundVar^{BoundVar} :]} .

The function Renum from CQC-WFF into CQC-WFF^{[: , BoundVar^{BoundVar} :]} is defined by the conditions (Def.6). (Def.6) (i) Renum(VERUM) = [: , BoundVar^{BoundVar} :] ⟼ VERUM,

(ii) for every k and for every variables list l of k and for every k-ary

predicate symbol P holds Renum(P [l]) = ATOM(P, l), (iii) for all r, s, x and for all functions f, g from [: , BoundVar^{BoundVar} :]

into CQC-WFF such that f = Renum(r) and g = Renum(s) holds Renum(¬r) = NEG(f) and Renum(r ∧ s) = CON(f, g, the number of quantifiers in r) and Renum(∀_{x}r) = UNIV(x, f).

Let us consider p, k, f. The functor Renum_{k,f}(p) yields an element of CQC-WFF and is defined by:

(Def.7) Renum_{k,f}(p) = Renum(p)(⟨⟨k, f⟩⟩).

Next we state several propositions:

(14) The number of quantifiers in VERUM = 0.

(15) The number of quantifiers in P [l_{1}] = 0.

(16) The number of quantifiers in ¬p = the number of quantifiers in p.

(17) The number of quantifiers in p ∧ q = (the number of quantifiers in p) + (the number of quantifiers in q).

(18) The number of quantifiers in ∀_{x}p = (the number of quantifiers in p)+1. Let A be a non-empty subset of . The functor min A yields a natural

number and is defined by: (Def.8) min A ∈ A and for every k such that k ∈ A holds min A ≤ k.

We now state two propositions:

(19) For all non-empty subsets A, B of such that A ⊆ B holds min B ≤ min A.

(20) For every element p of WFF holds snb(p) is finite.

The scheme MaxFinDomElem concerns a non-empty set A, a set B, and a binary predicate P, and states that:

there exists an element x of A such that x ∈ B and for every element y of A such that y ∈ B holds P[x, y] provided the parameters meet the following requirements:

• B is finite and B ≠ ∅ and B ⊆ A,

• for all elements x, y of A holds P[x, y] or P[y, x],

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

Let us consider p. The functor NBI(p) yielding a non-empty subset of is defined as follows: (Def.9) NBI(p) = {k : ⋀_{i}[k ≤ i ⇒ x_{i} ∉ snb(p)]}.

Let us consider p. The functor |• : p|_{}yielding a natural number is defined as follows:

(Def.10) |• : p|_{}= min NBI(p).

Next we state several propositions:

(21) |• : p|_{}= 0 if and only if p is closed.

(22) If x_{i} ∈ snb(p), then i < |• : p|_{}.

(23) |• : VERUM |_{}= 0.

(24) |• : ¬p|_{}= |• : p|_{}.

(25) |• : p|_{}≤ |• : p ∧ q|_{}and |• : q|_{}≤ |• : p ∧ q|_{}.

Let C be a non-empty set, and let D be a non-empty subset of C. Then id_{D} is an element of D^{D}.

Let us consider p. The functor p with variables separated yielding an element of CQC-WFF is defined as follows:

(Def.11) p with variables separated = Renum_{|•:p|_{},id_{BoundVar}}(p).

The following proposition is true

(26) VERUM with variables separated = VERUM.

The scheme CQCInd deals with a unary predicate P, and states that: for every r holds P[r]

provided the following requirements are met:

• P[VERUM],

• for every k and for every variables list l of k and for every k-ary predicate symbol P holds P[P [l]],

• for every r such that P[r] holds P[¬r],

• for all r, s such that P[r] and P[s] holds P[r ∧ s],

• for all r, x such that P[r] holds P[∀_{x}r]. We now state four propositions:

(27) P [l_{1}] with variables separated = P [l_{1}].

(28) If p is atomic, then p with variables separated = p.

(29) ¬p with variables separated = ¬(p with variables separated).

(30) If p is negative and q = Arg(p), then p with variables separated =

¬(q with variables separated). Let us consider p, and let X be a subset of [: CQC-WFF, , Fin BoundVar,

BoundVar^{BoundVar} :]. We say that X is closed w.r.t. p if and only if the conditions (Def.12) is satisfied.

(Def.12) (i) ⟨⟨p, |• : p|_{}, ∅_{BoundVar}, id_{BoundVar}⟩⟩ ∈ X, (ii) for all q, k, K, f such that ⟨⟨¬q, k, K, f⟩⟩ ∈ X holds ⟨⟨q, k, K, f⟩⟩ ∈ X, (iii) for all q, r, k, K, f such that ⟨⟨q ∧r, k, K, f⟩⟩ ∈ X holds ⟨⟨q, k, K, f⟩⟩ ∈ X

and ⟨⟨r, k + the number of quantifiers in q, K, f⟩⟩ ∈ X, (iv) for all q, x, k, K, f such that ⟨⟨∀_{x}q, k, K, f⟩⟩ ∈ X holds ⟨⟨q, k + 1, K ∪

{x}, f +· ({x} ⟼ x_{k})⟩⟩ ∈ X.

Let D be a non-empty set, and let x be an element of D. Then {x} is an element of Fin D.

Let us consider p. The functor Quadruples_{p} yields a subset of [: CQC-WFF, , Fin BoundVar, BoundVar^{BoundVar} :] and is defined by:

(Def.13) Quadruples_{p} is closed w.r.t. p and for every subset D of [: CQC-WFF, , Fin BoundVar, BoundVar^{BoundVar} :] such that D is closed w.r.t. p holds Quadruples_{p} ⊆ D.

One can prove the following propositions:

(31) ⟨⟨p, |• : p|_{}, ∅_{BoundVar}, id_{BoundVar}⟩⟩ ∈ Quadruples_{p}.

(32) For all q, k, K, f such that ⟨⟨¬q, k, K, f⟩⟩ ∈ Quadruples_{p} holds ⟨⟨q, k, K, f⟩⟩ ∈ Quadruples_{p}.

(33) For all q, r, k, K, f such that ⟨⟨q ∧ r, k, K, f⟩⟩ ∈ Quadruples_{p} holds ⟨⟨q, k, K, f⟩⟩ ∈ Quadruples_{p} and ⟨⟨r, k + the number of quantifiers in q, K, f⟩⟩ ∈ Quadruples_{p}.

(34) For all q, x, k, K, f such that ⟨⟨∀_{x}q, k, K, f⟩⟩ ∈ Quadruples_{p} holds ⟨⟨q, k + 1, K ∪ {x}, f +· ({x} ⟼ x_{k})⟩⟩ ∈ Quadruples_{p}.

(35) Suppose ⟨⟨q, k, K, f⟩⟩ ∈ Quadruples_{p}. Then (i) ⟨⟨q, k, K, f⟩⟩ = ⟨⟨p, |• : p|_{}, ∅_{BoundVar}, id_{BoundVar}⟩⟩, or (ii) ⟨⟨¬q, k, K, f⟩⟩ ∈ Quadruples_{p}, or (iii) there exists r such that ⟨⟨q ∧ r, k, K, f⟩⟩ ∈ Quadruples_{p}, or (iv) there exist r, l such that k = l + the number of quantifiers in r and

⟨⟨r ∧ q, l, K, f⟩⟩ ∈ Quadruples_{p}, or

(v) there exist x, l, h such that l + 1 = k and h +· ({x} ⟼ x_{l}) = f but ⟨⟨∀_{x}q, l, K, h⟩⟩ ∈ Quadruples_{p} or ⟨⟨∀_{x}q, l, K \ {x}, h⟩⟩ ∈ Quadruples_{p}.

The scheme Sep regression deals with an element A of CQC-WFF, and a 4-ary predicate P, and states that:

for all q, k, K, f such that ⟨⟨q, k, K, f⟩⟩ ∈ Quadruples_{A} holds P[q, k, K, f] provided the following conditions are met:

• P[A, |• : A|_{}, ∅_{BoundVar}, id_{BoundVar}],

• for all q, k, K, f such that ⟨⟨¬q, k, K, f⟩⟩ ∈ Quadruples_{A} and P[¬q, k, K, f] holds P[q, k, K, f],

• for all q, r, k, K, f such that ⟨⟨q ∧ r, k, K, f⟩⟩ ∈ Quadruples_{A} and P[q ∧ r, k, K, f] holds P[q, k, K, f] and P[r, k + the number of quantifiers in q, K, f],

• for all q, x, k, K, f such that ⟨⟨∀_{x}q, k, K, f⟩⟩ ∈ Quadruples_{A} and P[∀_{x}q, k, K, f] holds P[q, k + 1, K ∪ {x}, f +· ({x} ⟼ x_{k})].

We now state a number of propositions:

(36) For all q, k, K, f such that ⟨⟨q, k, K, f⟩⟩ ∈ Quadruples_{p} holds q is a subformula of p.

(37) Quadruples_{VERUM} = {⟨⟨ VERUM, 0, ∅_{BoundVar}, id_{BoundVar}⟩⟩}.

(38) For every k and for every variables list l of k and for every k-ary predicate symbol P holds Quadruples_{P [l]} = {⟨⟨P [l], |• : P [l]|_{}, ∅_{BoundVar}, id_{BoundVar}⟩⟩}.

(39) For all q, k, K, f such that ⟨⟨q, k, K, f⟩⟩ ∈ Quadruples_{p} holds snb(q) ⊆ snb(p) ∪ K.

(40) If ⟨⟨q, m, K, f⟩⟩ ∈ Quadruples_{p} and x_{i} ∈ f ^{∘} K, then i < m.

(41) If ⟨⟨q, m, K, f⟩⟩ ∈ Quadruples_{p}, then x_{m} ∉ f ^{∘} K.

(42) If ⟨⟨q, m, K, f⟩⟩ ∈ Quadruples_{p} and x_{i} ∈ f ^{∘} snb(p), then i < m.

(43) If ⟨⟨q, m, K, f⟩⟩ ∈ Quadruples_{p} and x_{i} ∈ f ^{∘} snb(q), then i < m.

(44) If ⟨⟨q, m, K, f⟩⟩ ∈ Quadruples_{p}, then x_{m} ∉ f ^{∘} snb(q).

(45) snb(p) = snb(p with variables separated).

(46) |• : p|_{}= |• : p with variables separated |_{}.

Let us consider p, q. We say that p and q are similar if and only if: (Def.14) p with variables separated = q with variables separated.

One can prove the following propositions:

(47) p and p are similar.

(48) If p and q are similar, then q and p are similar.

(49) If p and q are similar and q and r are similar, then p and r are similar.

References

[1] Grzegorz Bancerek. Connectives and subformulae of the first order language. Formalized Mathematics, 1(3):451–458, 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, 1990.

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

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

642 agata darmochwał and andrzej trybulec

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

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

[9] Czesław Byliński and Grzegorz Bancerek. Variables in formulae of the first order language. Formalized Mathematics, 1(3):459–469, 1990.

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

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

[12] Włodzimierz Lesisz and Witold A. Pogorzelski. A simplified definition of the notion of similarity between formulas of the first order predicate calculus. Reports on Mathematical Logic, (7):63–69, 1976.

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

[14] Witold A. Pogorzelski. Klasyczny Rachunek Predykatów. PWN, Warszawa, 1981.

[15] Witold A. Pogorzelski and Tadeusz Prucnal. The substitution rule for predicate letters in the first-order predicate calculus. Reports on Mathematical Logic, (5):77–90, 1975.

[16] Helena Rasiowa and Roman Sikorski. The Mathematics of Metamathematics. Volume 41 of Monografie Matematyczne, PWN, Warszawa, 1968.

[17] Piotr Rudnicki and Andrzej Trybulec. A first order language. Formalized Mathematics, 1(2):303–311, 1990.

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

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

[20] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

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

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

[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 and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

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

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

Category of Rings

Michał Muzalewski Warsaw University Białystok

Summary. We define the category of non-associative rings. The carriers of the rings are included in a universum. The universum is a parameter of the category.

MML Identifier: RINGCAT1.

The papers [14], [2], [15], [3], [1], [12], [7], [8], [5], [4], [13], [11], [6], [10], and [9] provide the terminology and notation for this paper. For simplicity we follow a convention: x, y will be arbitrary, D will be a non-empty set, U_{1} will be a universal class, and G, H will be field structures. Let us consider G, H. A map from G into H is a function from the carrier of G into the carrier of H.

Let G_{1}, G_{2}, G_{3} be field structures, and let f be a map from G_{1} into G_{2}, and let g be a map from G_{2} into G_{3}. Then g · f is a map from G_{1} into G_{3}.

Let us consider G. The functor id_{G} yields a map from G into G and is defined by: (Def.1) id_{G} = id_{(the carrier of G)}.

The following propositions are true:

(1) For every scalar x of G holds id_{G}(x) = x.

(2) For every map f from G into H holds f · id_{G} = f and id_{H} · f = f. Let us consider G, H. A map from G into H is linear if:

(Def.2) for all scalars x, y of G holds it(x + y) = it(x) + it(y) and for all scalars x, y of G holds it(x · y) = it(x) · it(y) and it(1_{G}) = 1_{H}.

We now state the proposition

(3) For all G_{1}, G_{2}, G_{3} being field structures and for every map f from G_{1} into G_{2} and for every map g from G_{2} into G_{3} such that f is linear and g is linear holds g · f is linear.

We consider ring morphisms structures which are systems ⟨a dom-map, a cod-map, a Fun⟩,

where the dom-map, the cod-map are a ring and the Fun is a map from the dom-map into the cod-map.

We now define three new functors. Let us consider f. The functor dom f yields a ring and is defined by: (Def.3) dom f = the dom-map of f. The functor cod f yields a ring and is defined by: (Def.4) cod f = the cod-map of f. The functor fun f yields a map from the dom-map of f into the cod-map of f and is defined by: (Def.5) fun f = the Fun of f.

In the sequel G, H, G_{1}, G_{2}, G_{3}, G_{4} will denote rings. A ring morphisms structure is called a morphism of rings if: (Def.6) fun it is linear.

Let us consider G. The functor I_{G} yields a strict morphism of rings and is defined as follows: (Def.7) I_{G} = ⟨G, G, id_{G}⟩.

Let us consider G, H. The predicate G ≤ H is defined as follows: (Def.8) there exists a morphism F of rings such that dom F = G and cod F =

H.

We now state the proposition

(4) G ≤ G. Let us consider G, H. Let us assume that G ≤ H. A strict morphism of

rings is said to be a morphism from G to H if: (Def.9) dom it = G and cod it = H.

Let us consider G. Then I_{G} is a strict morphism from G to G. We now state three propositions:

(5) For all morphisms g, f of rings such that dom g = cod f there exist G_{1}, G_{2}, G_{3} such that G_{1} ≤ G_{2} and G_{2} ≤ G_{3} and the ring morphisms structure of g is a morphism from G_{2} to G_{3} and the ring morphisms structure of f is a morphism from G_{1} to G_{2}.

(6) For every strict morphism F of rings holds F is a morphism from dom F to cod F and dom F ≤ cod F.

(7) For every strict morphism F of rings there exist G, H and there exists a map f from G into H such that F is a morphism from G to H and F = ⟨G, H, f⟩ and f is linear.

Let G, F be morphisms of rings. Let us assume that dom G = cod F. The functor G · F yields a strict morphism of rings and is defined by:

(Def.10) for all G_{1}, G_{2}, G_{3} and for every map g from G_{2} into G_{3} and for every map f from G_{1} into G_{2} such that the ring morphisms structure of G = ⟨G_{2}, G_{3}, g⟩ and the ring morphisms structure of F = ⟨G_{1}, G_{2}, f⟩ holds G · F = ⟨G_{1}, G_{3}, g · f⟩.

We now state two propositions:

(8) If G_{1} ≤ G_{2} and G_{2} ≤ G_{3}, then G_{1} ≤ G_{3}.

(9) For every morphism G from G_{2} to G_{3} and for every morphism F from G_{1} to G_{2} such that G_{1} ≤ G_{2} and G_{2} ≤ G_{3} holds G · F is a morphism from G_{1} to G_{3}.

Let us consider G_{1}, G_{2}, G_{3}, and let G be a morphism from G_{2} to G_{3}, and let F be a morphism from G_{1} to G_{2}. Let us assume that G_{1} ≤ G_{2} and G_{2} ≤ G_{3}. The functor F [G] yields a strict morphism from G_{1} to G_{3} and is defined as follows:

(Def.11) F [G] = G · F.

The following propositions are true:

(10) For all strict morphisms f, g of rings such that dom g = cod f there exist G_{1}, G_{2}, G_{3} and there exists a map f_{0} from G_{1} into G_{2} and there exists a map g_{0} from G_{2} into G_{3} such that f = ⟨G_{1}, G_{2}, f_{0}⟩ and g = ⟨G_{2}, G_{3}, g_{0}⟩ and g · f = ⟨G_{1}, G_{3}, g_{0} · f_{0}⟩.

(11) For all strict morphisms f, g of rings such that dom g = cod f holds dom(g · f) = dom f and cod(g · f) = cod g.

(12) For every morphism f from G_{1} to G_{2} and for every morphism g from G_{2} to G_{3} and for every morphism h from G_{3} to G_{4} such that G_{1} ≤ G_{2} and G_{2} ≤ G_{3} and G_{3} ≤ G_{4} holds h · (g · f) = (h · g) · f.

(13) For all strict morphisms f, g, h of rings such that dom h = cod g and dom g = cod f holds h · (g · f) = (h · g) · f.

(14) dom(I_{G}) = G and cod(I_{G}) = G and for every strict morphism f of rings such that cod f = G holds I_{G} · f = f and for every strict morphism g of rings such that dom g = G holds g · I_{G} = g.

A non-empty set is said to be a non-empty set of rings if: (Def.12) for every element x of it holds x is a strict ring.

In the sequel V denotes a non-empty set of rings. Let us consider V. We see that the element of V is a ring.

One can prove the following two propositions:

(15) For every strict morphism f of rings and for every element x of {f} holds x is a strict morphism of rings.

(16) For every morphism f from G to H and for every element x of {f}

holds x is a morphism from G to H. A non-empty set is said to be a non-empty set of morphisms of rings if:

(Def.13) for every element x of it holds x is a strict morphism of rings.

Let M be a non-empty set of morphisms of rings. We see that the element of M is a morphism of rings.

Next we state the proposition

(17) For every strict morphism f of rings holds {f} is a non-empty set of

morphisms of rings. Let us consider G, H. A non-empty set of morphisms of rings is called a

non-empty set of morphisms from G into H if: (Def.14) for every element x of it holds x is a morphism from G to H.

The following two propositions are true:

(18) D is a non-empty set of morphisms from G into H if and only if for every element x of D holds x is a morphism from G to H.

(19) For every morphism f from G to H holds {f} is a non-empty set of

morphisms from G into H. Let us consider G, H. Let us assume that G ≤ H. The functor Morphs(G, H)

yielding a non-empty set of morphisms from G into H is defined by: (Def.15) x ∈ Morphs(G, H) if and only if x is a morphism from G to H.

Let us consider G, H, and let M be a non-empty set of morphisms from G into H. We see that the element of M is a morphism from G to H.

Let us consider x, y. The predicate P_{ob} x, y is defined by the condition (Def.16).

(Def.16) There exist arbitrary x_{1}, x_{2}, x_{3}, x_{4}, x_{5}, x_{6} such that x = ⟨⟨⟨⟨x_{1}, x_{2}, x_{3}, x_{4}⟩⟩, x_{5}, x_{6}⟩⟩ and there exists a strict ring G such that y = G and x_{1} = the carrier of G and x_{2} = the addition of G and x_{3} = the reverse-map of G and x_{4} = the zero of G and x_{5} = the multiplication of G and x_{6} = the unity of G.

We now state two propositions:

(20) For arbitrary x, y_{1}, y_{2} such that P_{ob} x, y_{1} and P_{ob} x, y_{2} holds y_{1} = y_{2}.

(21) There exists x such that x ∈ U_{1} and P_{ob} x, Z_{3}.

Let us consider U_{1}. The functor RingObj(U_{1}) yielding a non-empty set is defined as follows:

(Def.17) for every y holds y ∈ RingObj(U_{1}) if and only if there exists x such that x ∈ U_{1} and P_{ob} x, y.

We now state two propositions:

(22) Z_{3} ∈ RingObj(U_{1}).

(23) For every element x of RingObj(U_{1}) holds x is a strict ring. Let us consider U_{1}. Then RingObj(U_{1}) is a non-empty set of rings. Let us consider V. The functor Morphs V yielding a non-empty set of mor-

phisms of rings is defined as follows: (Def.18) x ∈ Morphs V if and only if there exist elements G, H of V such that

G ≤ H and x is a morphism from G to H.

Let us consider V, and let F be an element of Morphs V. Then dom F is an element of V. Then cod F is an element of V.

Let us consider V, and let G be an element of V. The functor I_{G} yields a strict element of Morphs V and is defined by:

(Def.19) I_{G} = I_{G}.

We now define three new functors. Let us consider V. The functor dom V yields a function from Morphs V into V and is defined as follows:

(Def.20) for every element f of Morphs V holds (dom V)(f) = dom f. The functor cod V yielding a function from Morphs V into V is defined as follows:

(Def.21) for every element f of Morphs V holds (cod V)(f) = cod f.

The functor I_{V} yields a function from V into Morphs V and is defined by: (Def.22) for every element G of V holds I_{V} (G) = I_{G}.

We now state two propositions:

(24) For all elements g, f of Morphs V such that dom g = cod f there exist elements G_{1}, G_{2}, G_{3} of V such that G_{1} ≤ G_{2} and G_{2} ≤ G_{3} and g is a morphism from G_{2} to G_{3} and f is a morphism from G_{1} to G_{2}.

(25) For all elements g, f of Morphs V such that dom g = cod f holds g ·f ∈

Morphs V. Let us consider V. The functor comp V yielding a partial function from

[: Morphs V, Morphs V :] to Morphs V is defined as follows: (Def.23) for all elements g, f of Morphs V holds ⟨⟨g, f⟩⟩ ∈ dom comp V if and

only if dom g = cod f and for all elements g, f of Morphs V such that ⟨⟨g, f⟩⟩ ∈ dom comp V holds (comp V)(⟨⟨g, f⟩⟩) = g · f.

Let us consider U_{1}. The functor RingCat(U_{1}) yielding a strict category structure is defined by:

(Def.24) RingCat(U_{1}) = ⟨RingObj(U_{1}), Morphs RingObj(U_{1}), dom RingObj(U_{1}), cod RingObj(U_{1}), comp RingObj(U_{1}), I_{RingObj(U_{1})}⟩.

The following propositions are true:

(26) For all morphisms f, g of RingCat(U_{1}) holds ⟨⟨g, f⟩⟩ ∈ dom (the composition of RingCat(U_{1})) if and only if dom g = cod f.

(27) For every morphism f of RingCat(U_{1}) and for every element f′ of Morphs RingObj(U_{1}) and for every object b of RingCat(U_{1}) and for every element b′ of RingObj(U_{1}) holds f is a strict element of Morphs RingObj(U_{1}) and f′ is a morphism of RingCat(U_{1}) and b is a strict element of RingObj(U_{1}) and b′ is an object of RingCat(U_{1}).

(28) For every object b of RingCat(U_{1}) and for every element b′ of RingObj(U_{1}) such that b = b′ holds id_{b} = I_{b′}.

648 michał muzalewski

(29) For every morphism f of RingCat(U_{1}) and for every element f′ of Morphs RingObj(U_{1}) such that f = f′ holds dom f = dom f′ and cod f = cod f′.

(30) Let f, g be morphisms of RingCat(U_{1}). Let f′, g′ be elements of

Morphs RingObj(U_{1}). Suppose f = f′ and g = g′. Then

(i) dom g = cod f if and only if dom g′ = cod f′, (ii) dom g = cod f if and only if ⟨⟨g′, f′⟩⟩ ∈ dom comp RingObj(U_{1}), (iii) if dom g = cod f, then g · f = g′ · f′, (iv) dom f = dom g if and only if dom f′ = dom g′,

(v) cod f = cod g if and only if cod f′ = cod g′. Let us consider U_{1}. Then RingCat(U_{1}) is a strict category.

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. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

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

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

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

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

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

[9] Michał Muzalewski. Rings and modules - part II. Formalized Mathematics, 2(4):579– 585, 1991.

[10] Michał Muzalewski and Wojciech Skaba. Groups, rings, left- and right-modules. Formalized Mathematics, 2(2):275–278, 1991.

[11] Bogdan Nowak and Grzegorz Bancerek. Universal classes. Formalized Mathematics, 1(3):595–600, 1990.

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

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

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

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

Category of Left Modules

Michał Muzalewski Warsaw University Białystok

Summary. We define the category of left modules over an associative ring. The carriers of the modules are included in a universum. The universum is a parameter of the category.

MML Identifier: MODCAT 1.

The papers [12], [1], [2], [4], [5], [7], [3], [11], [10], [9], [6], and [8] provide the terminology and notation for this paper. For simplicity we adopt the following convention: x, y are arbitrary, D is a non-empty set, U_{1} is a universal class, R is an associative ring, and G, H are left modules over R. Let us consider R. A non-empty set is said to be a non-empty set of left-modules of R if: (Def.1) for every element x of it holds x is a strict left module over R.

In the sequel V is a non-empty set of left-modules of R. Let us consider R, V. We see that the element of V is a left module over R.

We now state two propositions:

(1) For every left module morphism f of R and for every element x of {f} holds x is a left module morphism of R.

(2) For every strict morphism f from G to H and for every element x of {f} holds x is a strict morphism from G to H.

Let us consider R. A non-empty set is said to be a non-empty set of morphisms of left-modules of R if: (Def.2) for every element x of it holds x is a strict left module morphism of R.

Let us consider R, and let M be a non-empty set of morphisms of left-modules of R. We see that the element of M is a left module morphism of R.

Next we state the proposition

(3) For every strict left module morphism f of R holds {f} is a non-empty set of morphisms of left-modules of R.

Let us consider R, G, H. A non-empty set of morphisms of left-modules of R is called a non-empty set of morphisms of left-modules from G into H if: (Def.3) for every element x of it holds x is a strict morphism from G to H.

The following two propositions are true:

(4) D is a non-empty set of morphisms of left-modules from G into H if and only if for every element x of D holds x is a strict morphism from G to H.

(5) For every strict morphism f from G to H holds {f} is a non-empty set of morphisms of left-modules from G into H.

Let us consider R, G, H. The functor Morphs(G, H) yields a non-empty set of morphisms of left-modules from G into H and is defined as follows: (Def.4) x ∈ Morphs(G, H) if and only if x is a strict morphism from G to H.

Let us consider R, G, H, and let M be a non-empty set of morphisms of left-modules from G into H. We see that the element of M is a morphism from G to H.

Let us consider x, y, R. The predicate P_{ob} x, y, R is defined by: (Def.5) there exist arbitrary x_{1}, x_{2} such that x = ⟨⟨x_{1}, x_{2}⟩⟩ and there exists a

strict left module G over R such that y = G and x_{1} = the carrier of G and x_{2} = the left multiplication of G.

One can prove the following propositions:

(6) For arbitrary x, y_{1}, y_{2} such that P_{ob} x, y_{1}, R and P_{ob} x, y_{2}, R holds y_{1} = y_{2}.

(7) For every U_{1} there exists x such that x ∈ {⟨⟨G, f⟩⟩}, where G ranges over elements of GroupObj(U_{1}), and f ranges over elements of {∅}^{[: the carrier of R, {∅}:]} and P_{ob} x,_{R}Θ, R.

Let us consider U_{1}, R. The functor LModObj(U_{1}, R) yielding a non-empty set is defined as follows: (Def.6) for every y holds y ∈ LModObj(U_{1}, R) if and only if there exists x such

that x ∈ {⟨⟨G, f⟩⟩}, where G ranges over elements of GroupObj(U_{1}), and f ranges over elements of {∅}^{[: the carrier of R, {∅}:]} and P_{ob} x, y, R.

One can prove the following two propositions:

(8) _{R}Θ ∈ LModObj(U_{1}, R).

(9) For every element x of LModObj(U_{1}, R) holds x is a strict left module over R.

Let us consider U_{1}, R. Then LModObj(U_{1}, R) is a non-empty set of leftmodules of R.

Let us consider R, V. The functor Morphs V yields a non-empty set of morphisms of left-modules of R and is defined as follows: (Def.7) for every x holds x ∈ Morphs V if and only if there exist strict elements

G, H of V such that x is a strict morphism from G to H.

We now define two new functors. Let us consider R, V, and let F be an element of Morphs V. The functor dom′ F yields an element of V and is defined as follows: (Def.8) dom′ F = dom F. The functor cod′ F yields an element of V and is defined by: (Def.9) cod′ F = cod F.

Let us consider R, V, and let G be an element of V. The functor I_{G} yielding a strict element of Morphs V is defined as follows:

(Def.10) I_{G} = I_{G}.

We now define three new functors. Let us consider R, V. The functor dom V yields a function from Morphs V into V and is defined by:

(Def.11) for every element f of Morphs V holds (dom V)(f) = dom′ f.

The functor cod V yields a function from Morphs V into V and is defined as follows:

(Def.12) for every element f of Morphs V holds (cod V)(f) = cod′ f.

The functor I_{V} yields a function from V into Morphs V and is defined by: (Def.13) for every element G of V holds I_{V} (G) = I_{G}.

One can prove the following three propositions:

(10) For all elements g, f of Morphs V such that dom′ g = cod′ f there exist strict elements G_{1}, G_{2}, G_{3} of V such that g is a morphism from G_{2} to G_{3} and f is a morphism from G_{1} to G_{2}.

(11) For all elements g, f of Morphs V such that dom′ g = cod′ f holds g · f ∈ Morphs V.

(12) For all elements g, f of Morphs V such that dom g = cod f holds g ·f ∈

Morphs V. Let us consider R, V. The functor comp V yields a partial function from

[: Morphs V, Morphs V :] to Morphs V and is defined by: (Def.14) for all elements g, f of Morphs V holds ⟨⟨g, f⟩⟩ ∈ dom comp V if and

only if dom′ g = cod′ f and for all elements g, f of Morphs V such that ⟨⟨g, f⟩⟩ ∈ dom comp V holds (comp V)(⟨⟨g, f⟩⟩) = g · f.

The following proposition is true

(13) For all elements g, f of Morphs V holds ⟨⟨g, f⟩⟩ ∈ dom comp V if and

only if dom g = cod f. Let us consider U_{1}, R. The functor LModCat(U_{1}, R) yields a strict category

structure and is defined by: (Def.15) LModCat(U_{1}, R) = ⟨LModObj(U_{1}, R), Morphs LModObj(U_{1}, R), dom LModObj(U_{1}, R),

cod LModObj(U_{1}, R), comp LModObj(U_{1}, R), I_{LModObj(U_{1},R)}⟩.

One can prove the following propositions:

(14) For all morphisms f, g of LModCat(U_{1}, R) holds ⟨⟨g, f⟩⟩ ∈ dom (the composition of LModCat(U_{1}, R)) if and only if dom g = cod f.

652 michał muzalewski

(15) Let f be a morphism of LModCat(U_{1}, R). Then for every element f′ of Morphs LModObj(U_{1}, R) and for every object b of LModCat(U_{1}, R) and for every element b′ of LModObj(U_{1}, R) holds f is a strict element of Morphs LModObj(U_{1}, R) and f′ is a morphism of LModCat(U_{1}, R) and b is a strict element of LModObj(U_{1}, R) and b′ is an object of LModCat(U_{1}, R).

(16) For every object b of LModCat(U_{1}, R) and for every element b′ of LModObj(U_{1}, R) such that b = b′ holds id_{b} = I_{b′}.

(17) For every morphism f of LModCat(U_{1}, R) and for every element f′ of Morphs LModObj(U_{1}, R) such that f = f′ holds dom f = dom f′ and cod f = cod f′.

(18) Let f, g be morphisms of LModCat(U_{1}, R). Let f′, g′ be elements of

Morphs LModObj(U_{1}, R). Suppose f = f′ and g = g′. Then

(i) dom g = cod f if and only if dom g′ = cod f′, (ii) dom g = cod f if and only if ⟨⟨g′, f′⟩⟩ ∈ dom comp LModObj(U_{1}, R), (iii) if dom g = cod f, then g · f = g′ · f′, (iv) dom f = dom g if and only if dom f′ = dom g′,

(v) cod f = cod g if and only if cod f′ = cod g′. Let us consider U_{1}, R. Then LModCat(U_{1}, R) is a strict category.

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. Partial functions. Formalized Mathematics, 1(2):357–367, 1990.

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

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

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

[8] Michał Muzalewski. Rings and modules - part II. Formalized Mathematics, 2(4):579– 585, 1991.

[9] Michał Muzalewski and Wojciech Skaba. N-tuples and Cartesian products for n=5. Formalized Mathematics, 2(2):255–258, 1991.

[10] Bogdan Nowak and Grzegorz Bancerek. Universal classes. Formalized Mathematics, 1(3):595–600, 1990.

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

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

Real Function One-Side Differantiability

Ewa Burakowska Warsaw University Białystok

Beata Madras Warsaw University Białystok

Summary. We define real function one-side differantiability and one-side continuity. Main properties of one-side differentiability function are proved. Connections between one-side differential and differential real function at the point are demonstrated.

MML Identifier: FDIFF 3.

The terminology and notation used in this paper have been introduced in the following papers: [17], [2], [4], [1], [11], [5], [7], [14], [18], [3], [8], [9], [10], [16], [15], [12], [13], and [6]. For simplicity we follow the rules: h, h_{1}, h_{2} are real sequences convergent to 0, c is a constant real sequence, f, f_{1}, f_{2} are partial functions from to , x_{0}, r, r_{1}, g, g_{1}, g_{2} are real numbers, n is a natural number, and a is a sequence of real numbers. The following propositions are true:

(1) If there exists r such that r > 0 and [x_{0} − r, x_{0}] ⊆ dom f, then there exist h, c such that rng c = {x_{0}} and rng(h + c) ⊆ dom f and for every n holds h(n) < 0.

(2) If there exists r such that r > 0 and [x_{0}, x_{0} + r] ⊆ dom f, then there exist h, c such that rng c = {x_{0}} and rng(h + c) ⊆ dom f and for every n holds h(n) > 0.

(3) Suppose For all h, c such that rng c = {x_{0}} and rng(h+c) ⊆ dom f and for every n holds h(n) < 0 holds h^{−1} (f · (h + c) − f · c) is convergent and {x_{0}} ⊆ dom f. Given h_{1}, h_{2}, c. Suppose rng c = {x_{0}} and rng(h_{1} + c) ⊆ dom f and for every n holds h_{1}(n) < 0 and rng(h_{2} + c) ⊆ dom f and for every n holds h_{2}(n) < 0. Then lim(h_{1}^{−1} (f · (h_{1} + c) − f · c)) = lim(h_{2}^{−1} (f · (h_{2} + c) − f · c)).

(4) Suppose For all h, c such that rng c = {x_{0}} and rng(h+c) ⊆ dom f and for every n holds h(n) > 0 holds h^{−1} (f · (h + c) − f · c) is convergent and {x_{0}} ⊆ dom f. Given h_{1}, h_{2}, c. Suppose rng c = {x_{0}} and rng(h_{1} + c) ⊆ dom f and rng(h_{2} + c) ⊆ dom f and for every n holds h_{1}(n) > 0 and for every n holds h_{2}(n) > 0. Then lim(h_{1}^{−1} (f · (h_{1} + c) − f · c)) = lim(h_{2}^{−1} (f · (h_{2} + c) − f · c)).

We now define four new predicates. Let us consider f, x_{0}. We say that f is left continous in x_{0} if and only if: (Def.1) x_{0} ∈ dom f and for every a such that rng a ⊆ ]−∞, x_{0}[ ∩ dom f and a is

convergent and lim a = x_{0} holds f · a is convergent and f(x_{0}) = lim(f · a). We say that f is right continous in x_{0} if and only if: (Def.2) x_{0} ∈ dom f and for every a such that rng a ⊆ ]x_{0}, +∞[ ∩ dom f and a is

convergent and lim a = x_{0} holds f · a is convergent and f(x_{0}) = lim(f · a). We say that f is right differentiable in x_{0} if and only if the conditions (Def.3) is satisfied. (Def.3) (i) There exists r such that r > 0 and [x_{0}, x_{0} + r] ⊆ dom f,

(ii) for all h, c such that rng c = {x_{0}} and rng(h + c) ⊆ dom f and for

every n holds h(n) > 0 holds h^{−1} (f · (h + c) − f · c) is convergent. We say that f is left differentiable in x_{0} if and only if the conditions (Def.4) is satisfied. (Def.4) (i) There exists r such that r > 0 and [x_{0} − r, x_{0}] ⊆ dom f,

(ii) for all h, c such that rng c = {x_{0}} and rng(h + c) ⊆ dom f and for every n holds h(n) < 0 holds h^{−1} (f · (h + c) − f · c) is convergent.

One can prove the following propositions:

(5) If f is left differentiable in x_{0}, then f is left continous in x_{0}.

(6) Suppose f is left continous in x_{0} and f(x_{0}) ≠ g_{2} and there exists r such that r > 0 and [x_{0} − r, x_{0}] ⊆ dom f. Then there exists r_{1} such that r_{1} > 0 and [x_{0} − r_{1}, x_{0}] ⊆ dom f and for every g such that g ∈ [x_{0} − r_{1}, x_{0}] holds f(g) ≠ g_{2}.

(7) If f is right differentiable in x_{0}, then f is right continous in x_{0}.

(8) Suppose f is right continous in x_{0} and f(x_{0}) ≠ g_{2} and there exists r such that r > 0 and [x_{0}, x_{0} + r] ⊆ dom f. Then there exists r_{1} such that r_{1} > 0 and [x_{0}, x_{0} +r_{1}] ⊆ dom f and for every g such that g ∈ [x_{0}, x_{0} +r_{1}] holds f(g) ≠ g_{2}.

Let us consider x_{0}, f. Let us assume that f is left differentiable in x_{0}. The functor f′_{−}(x_{0}) yielding a real number is defined by: (Def.5) for all h, c such that rng c = {x_{0}} and rng(h + c) ⊆ dom f and for every

n holds h(n) < 0 holds f′_{−}(x_{0}) = lim(h^{−1} (f · (h + c) − f · c)).

Let us consider x_{0}, f. Let us assume that f is right differentiable in x_{0}. The functor f′_{+}(x_{0}) yields a real number and is defined by: (Def.6) for all h, c such that rng c = {x_{0}} and rng(h + c) ⊆ dom f and for every

n holds h(n) > 0 holds f′_{+}(x_{0}) = lim(h^{−1} (f · (h + c) − f · c)).

The following propositions are true:

(9) f is left differentiable in x_{0} and f′_{−}(x_{0}) = g if and only if the following conditions are satisfied:

(i) there exists r such that 0 < r and [x_{0} − r, x_{0}] ⊆ dom f, (ii) for all h, c such that rng c = {x_{0}} and rng(h + c) ⊆ dom f and for

every n holds h(n) < 0 holds h^{−1} (f · (h + c) − f · c) is convergent and lim(h^{−1} (f · (h + c) − f · c)) = g.

(10) If f_{1} is left differentiable in x_{0} and f_{2} is left differentiable in x_{0}, then f_{1} + f_{2} is left differentiable in x_{0} and (f_{1} + f_{2})′_{−}(x_{0}) = f_{1}′_{−}(x_{0}) + f_{2}′_{−}(x_{0}).

(11) If f_{1} is left differentiable in x_{0} and f_{2} is left differentiable in x_{0}, then f_{1} − f_{2} is left differentiable in x_{0} and (f_{1} − f_{2})′_{−}(x_{0}) = f_{1}′_{−}(x_{0}) − f_{2}′_{−}(x_{0}).

(12) If f_{1} is left differentiable in x_{0} and f_{2} is left differentiable in x_{0}, then f_{1} f_{2} is left differentiable in x_{0} and (f_{1} f_{2})′_{−}(x_{0}) = f_{1}′_{−}(x_{0}) · f_{2}(x_{0}) + f_{2}′_{−}(x_{0}) · f_{1}(x_{0}).

(13) If f_{1} is left differentiable in x_{0} and f_{2} is left differentiable in x_{0} and f_{2}(x_{0}) ≠ 0, then \frac{f_{1}}{f_{2}} is left differentiable in x_{0} and

(\frac{f_{1}}{f_{2}} )′_{−}(x_{0}) = \frac{f_{1}′_{−}(x_{0})·f_{2}(x_{0})−f_{2}′_{−}(x_{0})·f_{1}(x_{0})}{f_{2}(x_{0})2}.

(14) If f is left differentiable in x_{0} and f(x_{0}) ≠ 0, then \frac{1}{f} is left differentiable

in x_{0} and (\frac{1}{f})′_{−}(x_{0}) = −\frac{f′_{−}(x_{0})}{f(x_{0})2}.

(15) f is right differentiable in x_{0} and f′_{+}(x_{0}) = g_{1} if and only if the following

conditions are satisfied:

(i) there exists r such that r > 0 and [x_{0}, x_{0} + r] ⊆ dom f, (ii) for all h, c such that rng c = {x_{0}} and rng(h + c) ⊆ dom f and for

every n holds h(n) > 0 holds h^{−1} (f · (h + c) − f · c) is convergent and lim(h^{−1} (f · (h + c) − f · c)) = g_{1}.

(16) If f_{1} is right differentiable in x_{0} and f_{2} is right differentiable in x_{0}, then f_{1} +f_{2} is right differentiable in x_{0} and (f_{1} +f_{2})′_{+}(x_{0}) = f_{1}′_{+}(x_{0})+f_{2}′_{+}(x_{0}).

(17) If f_{1} is right differentiable in x_{0} and f_{2} is right differentiable in x_{0}, then f_{1} −f_{2} is right differentiable in x_{0} and (f_{1} −f_{2})′_{+}(x_{0}) = f_{1}′_{+}(x_{0})−f_{2}′_{+}(x_{0}).

(18) If f_{1} is right differentiable in x_{0} and f_{2} is right differentiable in x_{0}, then f_{1} f_{2} is right differentiable in x_{0} and (f_{1} f_{2})′_{+}(x_{0}) = f_{1}′_{+}(x_{0}) · f_{2}(x_{0}) + f_{2}′_{+}(x_{0}) · f_{1}(x_{0}).

(19) If f_{1} is right differentiable in x_{0} and f_{2} is right differentiable in x_{0} and f_{2}(x_{0}) ≠ 0, then \frac{f_{1}}{f_{2}} is right differentiable in x_{0} and (\frac{f_{1}}{f_{2}} )′_{+}(x_{0}) =

\frac{f_{1}′_{+}(x_{0})·f_{2}(x_{0})−f_{2}′_{+}(x_{0})·f_{1}(x_{0})}{f_{2}(x_{0})2}.

(20) If f is right differentiable in x_{0} and f(x_{0}) ≠ 0, then \frac{1}{f} is right differen-

tiable in x_{0} and (\frac{1}{f})′_{+}(x_{0}) = −\frac{f′_{+}(x_{0})}{f(x_{0})2} .

(21) If f is right differentiable in x_{0} and f is left differentiable in x_{0} and f′_{+}(x_{0}) = f′_{−}(x_{0}), then f is differentiable in x_{0} and f′(x_{0}) = f′_{+}(x_{0}) and f′(x_{0}) = f′_{−}(x_{0}).

656 ewa burakowska and beata madras

(22) If f is differentiable in x_{0}, then f is right differentiable in x_{0} and f is left differentiable in x_{0} and f′(x_{0}) = f′_{+}(x_{0}) and f′(x_{0}) = f′_{−}(x_{0}).

References

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

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

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

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

[5] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273–275, 1990.

[6] Jarosław Kotowicz. The limit of a real function at infinity. Formalized Mathematics, 2(1):17–28, 1991.

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

[8] Jarosław Kotowicz. Partial functions from a domain to a domain. Formalized Mathematics, 1(4):697–702, 1990.

[9] Jarosław Kotowicz. Partial functions from a domain to the set of real numbers. Formalized Mathematics, 1(4):703–709, 1990.

[10] Jarosław Kotowicz. Properties of real functions. Formalized Mathematics, 1(4):781–786, 1990.

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

[12] Jarosław Kotowicz and Konrad Raczkowski. Real function differentiability - Part II. Formalized Mathematics, 2(3):407–411, 1991.

[13] Andrzej Ne‘dzusiak. σ-fields and probability. Formalized Mathematics, 1(2):401–407, 1990.

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

[15] Konrad Raczkowski and Paweł Sadowski. Real function differentiability. Formalized Mathematics, 1(4):797–801, 1990.

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

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

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

Sequences in Metric Spaces

Stanisława Kanas Technical University of Rzeszów

Adam Lecko Technical University of Rzeszów

Summary. Sequences in metric spaces are defined. The article contains definitions of bounded, convergent, Cauchy sequences. The subsequences are introduced too. Some theorems concerning sequences are proved.

MML Identifier: METRIC 6.

The terminology and notation used in this paper have been introduced in the following articles: [11], [14], [4], [5], [3], [6], [13], [12], [7], [10], [8], [9], [1], and [2]. For simplicity we follow a convention: X will be a metric space, x, y, z will be elements of the carrier of X, V will be a subset of the carrier of X, A will be a non-empty set, a will be an element of A, G will be a function from [: A, A:] into , k, n, m will be natural numbers, and r will be a real number. The following propositions are true:

(1) |ρ(x, z) − ρ(y, z)| ≤ ρ(x, y).

(2) If G is a metric of A, then for all elements a, b of A holds 0 ≤ G(a, b). Let us consider A, G. We say that G is not a pseudo metric if and only if:

(Def.1) for all elements a, b of A holds G(a, b) = 0 if and only if a = b.

Let us consider A, G. We say that G is symmetric if and only if: (Def.2) for all elements a, b of A holds G(a, b) = G(b, a).

Let us consider A, G. We say that G satisfies triangle inequality if and only if: (Def.3) for all elements a, b, c of A holds G(a, c) ≤ G(a, b) + G(b, c).

Next we state three propositions:

(3) G is a metric of A if and only if G is not a pseudo metric and G is symmetric and G satisfies triangle inequality.

(4) For every strict metric space X holds the distance of X is not a pseudo metric and the distance of X is symmetric and the distance of X satisfies triangle inequality.

(5) G is a metric of A if and only if G is not a pseudo metric and for all elements a, b, c of A holds G(b, c) ≤ G(a, b) + G(a, c).

Let us consider A, G. Let us assume that G is a metric of A. The functor G̃_{A} yielding a function from [: A, A:] into is defined as follows: (Def.4) for all elements a, b of A holds G̃_{A}(a, b) = \frac{G(a, b)}{1+G(a, b)}.

The following proposition is true

(6) If G is a metric of A, then G̃_{A} is a metric of A. Let X be a metric space. A sequence of elements of X is defined by:

(Def.5) it is a function from into the carrier of X.

Let X be a metric space. We see that the sequence of elements of X is a function from into the carrier of X.

Next we state the proposition

(7) For every function F from into the carrier of X holds F is a sequence of elements of X.

We follow the rules: S, S_{1}, T denote sequences of elements of X, N_{1} denotes an increasing sequence of naturals, and F denotes a function from into the carrier of X. The following propositions are true:

(8) F is a sequence of elements of X if and only if for every a such that a ∈ holds F (a) is an element of the carrier of X.

(9) For all S, T such that for every n holds S(n) = T (n) holds S = T.

(10) For every x there exists S such that rng S = {x}.

(11) If there exists x such that for every n holds S(n) = x, then there exists

x such that rng S = {x}. Let us consider X, S. We say that S is constant if and only if:

(Def.6) there exists x such that for every n holds S(n) = x.

The following proposition is true (13)^{1} S is constant if and only if there exists x such that rng S = {x}.

Let us consider X, S. We say that S is convergent if and only if: (Def.7) there exists x such that for every r such that 0 < r there exists m such

that for every n such that m ≤ n holds ρ(S(n), x) < r. Let us consider X, S, x. We say that S is convergent to x if and only if:

(Def.8) for every r such that 0 < r there exists m such that for every n such

that m ≤ n holds ρ(S(n), x) < r. Let us consider X, S. We say that S satisfies the Cauchy condition if and

only if: (Def.9) for every r such that 0 < r there exists m such that for all n, k such

that m ≤ n and m ≤ k holds ρ(S(n), S(k)) < r. Let us consider X, V. We say that V is bounded if and only if:

1The proposition (12) has been removed.

(Def.10) there exist r, x such that 0 < r and V ⊆ Ball(x, r).

Let us consider X, S. We say that S is bounded if and only if: (Def.11) there exist r, x such that 0 < r and rng S ⊆ Ball(x, r).

Let us consider X, V, S. We say that V contains almost all sequence S if and only if:

(Def.12) there exists m such that for every n such that m ≤ n holds S(n) ∈ V.

Let us consider X, s_{1}, s_{2}. We say that s_{1} is a subsequence of s_{2} if and only if:

(Def.13) there exists N_{1} such that s_{1} = s_{2} · N_{1}.

Next we state the proposition (16)^{2} S is convergent to x if and only if for every r such that 0 < r there

exists m such that for every n such that m ≤ n holds ρ(S(n), x) < r. We now state three propositions:

(20)^{3} S is bounded if and only if there exist r, x such that 0 < r and for every

n holds S(n) ∈ Ball(x, r).

(21) If S is convergent to x, then S is convergent.

(22) If S is convergent, then there exists x such that S is convergent to x. Let us consider X, S, x. The functor ρ(S, x) yields a sequence of real numbers

and is defined as follows: (Def.14) for every n holds (ρ(S, x))(n) = ρ(S(n), x).

Next we state the proposition

(23) ρ(S, x) is a sequence of real numbers if and only if for every n holds

(ρ(S, x))(n) = ρ(S(n), x). Let us consider X, S, T. The functor ρ(S, T) yields a sequence of real

numbers and is defined by: (Def.15) for every n holds (ρ(S, T))(n) = ρ(S(n), T (n)).

Next we state the proposition

(24) ρ(S, T) is a sequence of real numbers if and only if for every n holds

(ρ(S, T))(n) = ρ(S(n), T (n)). Let us consider X, S. Let us assume that S is convergent. The functor lim S

yields an element of the carrier of X and is defined as follows: (Def.16) for every r such that 0 < r there exists m such that for every n such

that m ≤ n holds ρ(S(n), lim S) < r.

One can prove the following propositions:

(25) If S is convergent, then lim S = x if and only if for every r such that 0 < r there exists m such that for every n such that m ≤ n holds ρ(S(n), x) < r.

2The propositions (14) and (15) have been removed.

3The propositions (17)–(19) have been removed.

(26) If S is convergent to x, then lim S = x.

(27) S is convergent to x if and only if S is convergent and lim S = x.

(28) If S is convergent, then there exists x such that S is convergent to x and lim S = x.

(29) S is convergent to x if and only if ρ(S, x) is convergent and lim ρ(S, x) = 0.

(30) If S is convergent to x, then for every r such that 0 < r holds Ball(x, r) contains almost all sequence S.

(31) If for every r such that 0 < r holds Ball(x, r) contains almost all sequence S, then for every V such that x ∈ V and V ∈ the open set family of X holds V contains almost all sequence S.

(32) If for every V such that x ∈ V and V ∈ the open set family of X holds V contains almost all sequence S, then S is convergent to x.

(33) S is convergent to x if and only if for every r such that 0 < r holds Ball(x, r) contains almost all sequence S.

(34) S is convergent to x if and only if for every V such that x ∈ V and V ∈ the open set family of X holds V contains almost all sequence S.

(35) For every r such that 0 < r holds Ball(x, r) contains almost all sequence S if and only if for every V such that x ∈ V and V ∈ the open set family of X holds V contains almost all sequence S.

(36) If S is convergent and T is convergent, then ρ(lim S, lim T) = lim ρ(S, T).

(37) If S is convergent to x and S is convergent to y, then x = y.

(38) If S is constant, then S is convergent.

(39) If S is convergent to x and S_{1} is a subsequence of S, then S_{1} is convergent to x.

(40) If S satisfies the Cauchy condition and S_{1} is a subsequence of S, then S_{1} satisfies the Cauchy condition.

(41) If S is convergent, then S satisfies the Cauchy condition.

(42) If S is constant, then S satisfies the Cauchy condition.

(43) If S is convergent, then S is bounded.

(44) If S satisfies the Cauchy condition, then S is bounded.

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. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

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

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

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

sequences in metric spaces 661

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

[8] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273–275, 1990.

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

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

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

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

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

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

662

The Topological Space E_{T}^{2}. Simple Closed Curves

Agata Darmochwał Warsaw University Yatsuka Nakamura Shinshu University

Summary. Continuation of [13]. The fact that the unit square is compact is shown in the beginning of the article. Next the notion of simple closed curve is introduced. It is proved that any simple closed curve can be divided into two independent parts which are homeomorphic to unit interval .

MML Identifier: TOPREAL2.

The notation and terminology used here have been introduced in the following articles: [22], [21], [14], [1], [24], [20], [6], [7], [18], [4], [8], [23], [17], [25], [11], [16], [9], [19], [2], [5], [15], [3], [10], [12], and [13]. We follow the rules: p_{1}, p_{2}, q_{1}, q_{2} will denote points of E_{T}^{2} and P, Q, P_{1}, P_{2} will denote subsets of E_{T}^{2}. The following propositions are true:

(1) If p_{1} ≠ p_{2} and p_{1} ∈ _{E^{2}} and p_{2} ∈ _{E^{2}}, then there exist P_{1}, P_{2} such that P_{1} is an arc from p_{1} to p_{2} and P_{2} is an arc from p_{1} to p_{2} and _{E^{2}} = P_{1} ∪P_{2} and P_{1} ∩ P_{2} = {p_{1}, p_{2}}.

(2) _{E^{2}} is compact.

(3) For every map f from (E_{T}^{2}) Q into (E_{T}^{2}) P such that f is a homeomorphism and Q is an arc from q_{1} to q_{2} and P ≠ ∅ and for all p_{1}, p_{2} such that p_{1} = f(q_{1}) and p_{2} = f(q_{2}) holds P is an arc from p_{1} to p_{2}.

Let us consider P. We say that P is a simple closed curve if and only if: (Def.1) P ≠ ∅ and there exists a map f from (E_{T}^{2}) _{E^{2}} into (E_{T}^{2}) P such that

f is a homeomorphism.

Next we state two propositions:

(4) If P is a simple closed curve, then there exist p_{1}, p_{2} such that p_{1} ≠ p_{2} and p_{1} ∈ P and p_{2} ∈ P.

(5) P is a simple closed curve if and only if the following conditions are satisfied:

664 agata darmochwał and yatsuka nakamura

(i) there exist p_{1}, p_{2} such that p_{1} ≠ p_{2} and p_{1} ∈ P and p_{2} ∈ P, (ii) for all p_{1}, p_{2} such that p_{1} ≠ p_{2} and p_{1} ∈ P and p_{2} ∈ P there exist P_{1},

P_{2} such that P_{1} is an arc from p_{1} to p_{2} and P_{2} is an arc from p_{1} to p_{2} and P = P_{1} ∪ P_{2} and P_{1} ∩ P_{2} = {p_{1}, p_{2}}.

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] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481– 485, 1991.

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

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

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

[7] Czesław Byliński. 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] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383–386, 1990.

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

[11] Agata Darmochwał. Families of subsets, subspaces and mappings in topological spaces. Formalized Mathematics, 1(2):257–261, 1990.

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

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

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

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

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

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

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

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

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

[21] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

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

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

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

[25] Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231–237, 1990.

Separated and Weakly Separated Subspaces of Topological Spaces

Zbigniew Karno Warsaw University Białystok

Summary. A new concept of weakly separated subsets and subspaces of topological spaces is described in Mizar formalizm. Based on [1], in comparison with the notion of separated subsets (subspaces), some properties of such subsets (subspaces) are discussed. Some necessary facts concerning closed subspaces, open subspaces and the union and the meet of two subspaces are also introduced. To present the main theorems we first formulate basic definitions. Let X be a topological space. Two subsets A_{1} and A_{2} of X are called weakly separated if A_{1} \A_{2} and A_{2} \A_{1} are separated. Two subspaces X_{1} and X_{2} of X are called weakly separated if their carriers are weakly separated. The following theorem contains a useful characterization of weakly separated subsets in the special case when A_{1} ∪ A_{2} is equal to the carrier of X. A_{1} and A_{2} are weakly separated iff there are such subsets of X, C_{1} and C_{2} closed (open) and C open (closed, respectively), that A_{1} ∪ A_{2} = C_{1} ∪ C_{2} ∪ C, C_{1} ⊂ A_{1}, C_{2} ⊂ A_{2} and C ⊂ A_{1} ∩ A_{2}. Next theorem divided into two parts contains similar characterization of weakly separated subspaces in the special case when the union of X_{1} and X_{2} is equal to X. If X_{1} meets X_{2}, then X_{1} and X_{2} are weakly separated iff either X_{1} is a subspace of X_{2} or X_{2} is a subspace of X_{1} or there are such open (closed) subspaces Y_{1} and Y_{2} of X that Y_{1} is a subspace of X_{1} and Y_{2} is a subspace of X_{2} and either X is equal to the union of Y_{1} and Y_{2} or there is a(n) closed (open, respectively) subspace Y of X being a subspace of the meet of X_{1} and X_{2} and with the property that X is the union of all Y_{1}, Y_{2} and Y. If X_{1} misses X_{2}, then X_{1} and X_{2} are weakly separated iff X_{1} and X_{2} are open (closed) subspaces of X. Moreover, the following simple characterization of separated subspaces by means of weakly separated ones is obtained. X_{1} and X_{2} are separated iff there are weakly separated subspaces Y_{1} and Y_{2} of X such that X_{1} is a subspace of Y_{1}, X_{2} is a subspace of Y_{2} and either Y_{1} misses Y_{2} or the meet of Y_{1} and Y_{2} misses the union of X_{1} and X_{2}.

MML Identifier: TSEP 1.

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

1. Some properties of subspaces of topological spaces

In the sequel X is a topological space. We now state a number of propositions: (1) For every subspace X_{0} of X holds the carrier of X_{0} is a subset of X.

(2) X is a subspace of X.

(3) For every strict topological space X holds X Ω_{X} = X.

(4) For all subspaces X_{1}, X_{2} of X holds the carrier of X_{1} ⊆ the carrier of X_{2} if and only if X_{1} is a subspace of X_{2}.

(5) For all strict subspaces X_{1}, X_{2} of X holds the carrier of X_{1} = the carrier of X_{2} if and only if X_{1} = X_{2}.

(6) For all strict subspaces X_{1}, X_{2} of X holds X_{1} is a subspace of X_{2} and X_{2} is a subspace of X_{1} if and only if X_{1} = X_{2}.

(7) For every subspace X_{1} of X and for every subspace X_{2} of X_{1} holds X_{2} is a subspace of X.

(8) For every subspace X_{0} of X and for all subsets C, A of X and for every subset B of X_{0} such that C is closed and C ⊆ the carrier of X_{0} and A ⊆ C and A = B holds B is closed if and only if A is closed.

(9) For every subspace X_{0} of X and for all subsets C, A of X and for every subset B of X_{0} such that C is open and C ⊆ the carrier of X_{0} and A ⊆ C and A = B holds B is open if and only if A is open.

(10) For every non-empty subset A_{0} of X there exists a strict subspace X_{0} of X such that A_{0} = the carrier of X_{0}.

(11) For every subspace X_{0} of X and for every subset A of X such that A = the carrier of X_{0} holds X_{0} is a closed subspace of X if and only if A is closed.

(12) For every closed subspace X_{0} of X and for every subset A of X and for every subset B of X_{0} such that A = B holds B is closed if and only if A is closed.

(13) For every closed subspace X_{1} of X and for every closed subspace X_{2} of X_{1} holds X_{2} is a closed subspace of X.

(14) For every closed subspace X_{1} of X and for every subspace X_{2} of X such that the carrier of X_{1} ⊆ the carrier of X_{2} holds X_{1} is a closed subspace of X_{2}.

(15) For every non-empty subset A_{0} of X such that A_{0} is closed there exists a strict closed subspace X_{0} of X such that A_{0} = the carrier of X_{0}.

Let X be a topological space. A subspace of X is said to be an open subspace of X if:

(Def.1) for every subset A of X such that A = the carrier of it holds A is open.

The following propositions are true:

(16) For every subspace X_{0} of X and for every subset A of X such that A = the carrier of X_{0} holds X_{0} is an open subspace of X if and only if A is open.

(17) For every open subspace X_{0} of X and for every subset A of X and for every subset B of X_{0} such that A = B holds B is open if and only if A is open.

(18) For every open subspace X_{1} of X and for every open subspace X_{2} of X_{1} holds X_{2} is an open subspace of X.

(19) For every open subspace X_{1} of X and for every subspace X_{2} of X such that the carrier of X_{1} ⊆ the carrier of X_{2} holds X_{1} is an open subspace of X_{2}.

(20) For every non-empty subset A_{0} of X such that A_{0} is open there exists a strict open subspace X_{0} of X such that A_{0} = the carrier of X_{0}.

2. Operations on subspaces of topological spaces

In the sequel X denotes a topological space. Let us consider X, and let X_{1}, X_{2} be subspaces of X. The functor X_{1} ∪ X_{2} yielding a strict subspace of X is defined by: (Def.2) the carrier of X_{1} ∪ X_{2} = (the carrier of X_{1}) ∪ (the carrier of X_{2}).

In the sequel X_{1}, X_{2}, X_{3} will denote subspaces of X. One can prove the following propositions:

(21) X_{1} ∪ X_{2} = X_{2} ∪ X_{1} and (X_{1} ∪ X_{2}) ∪ X_{3} = X_{1} ∪ (X_{2} ∪ X_{3}).

(22) X_{1} is a subspace of X_{1} ∪ X_{2} and X_{2} is a subspace of X_{1} ∪ X_{2}.

(23) For all strict subspaces X_{1}, X_{2} of X holds X_{1} is a subspace of X_{2} if and only if X_{1} ∪ X_{2} = X_{2} but X_{2} is a subspace of X_{1} if and only if X_{1} ∪ X_{2} = X_{1}.

(24) For all closed subspaces X_{1}, X_{2} of X holds X_{1} ∪X_{2} is a closed subspace of X.

(25) For all open subspaces X_{1}, X_{2} of X holds X_{1} ∪ X_{2} is an open subspace

of X. We now define two new predicates. Let us consider X, and let X_{1}, X_{2} be

subspaces of X. We say that X_{1} misses X_{2} if and only if: (Def.3) (the carrier of X_{1}) ∩ (the carrier of X_{2}) = ∅. We say that X_{1} meets X_{2} if and only if: (Def.4) (the carrier of X_{1}) ∩ (the carrier of X_{2}) ≠ ∅.

The following three propositions are true:

(26) X_{1} misses X_{2} if and only if X_{1} does not meet X_{2}.

(27) X_{1} misses X_{2} if and only if X_{2} misses X_{1} but X_{1} meets X_{2} if and only if X_{2} meets X_{1}.

(28) For all subsets A_{1}, A_{2} of X such that A_{1} = the carrier of X_{1} and A_{2} = the carrier of X_{2} holds X_{1} misses X_{2} if and only if A_{1} misses A_{2} but X_{1} meets X_{2} if and only if A_{1} meets A_{2}.

Let us consider X, and let X_{1}, X_{2} be subspaces of X. Let us assume that X_{1} meets X_{2}. The functor X_{1} ∩ X_{2} yielding a strict subspace of X is defined by: (Def.5) the carrier of X_{1} ∩ X_{2} = (the carrier of X_{1}) ∩ (the carrier of X_{2}).

In the sequel X_{1}, X_{2}, X_{3} will denote subspaces of X. We now state several propositions:

(29) If X_{1} meets X_{2} or X_{2} meets X_{1}, then X_{1} ∩ X_{2} = X_{2} ∩ X_{1} but if X_{1} meets X_{2} and X_{1} ∩ X_{2} meets X_{3} or X_{2} meets X_{3} and X_{1} meets X_{2} ∩ X_{3}, then (X_{1} ∩ X_{2}) ∩ X_{3} = X_{1} ∩ (X_{2} ∩ X_{3}).

(30) If X_{1} meets X_{2}, then X_{1} ∩ X_{2} is a subspace of X_{1} and X_{1} ∩ X_{2} is a subspace of X_{2}.

(31) For all strict subspaces X_{1}, X_{2} of X such that X_{1} meets X_{2} holds X_{1} is a subspace of X_{2} if and only if X_{1} ∩ X_{2} = X_{1} but X_{2} is a subspace of X_{1} if and only if X_{1} ∩ X_{2} = X_{2}.

(32) For all closed subspaces X_{1}, X_{2} of X such that X_{1} meets X_{2} holds X_{1} ∩ X_{2} is a closed subspace of X.

(33) For all open subspaces X_{1}, X_{2} of X such that X_{1} meets X_{2} holds X_{1}∩X_{2} is an open subspace of X.

(34) If X_{1} meets X_{2}, then X_{1} ∩ X_{2} is a subspace of X_{1} ∪ X_{2}.

(35) For every subspace Y of X such that X_{1} meets Y or Y meets X_{1} but X_{2} meets Y or Y meets X_{2} holds (X_{1} ∪ X_{2}) ∩ Y = X_{1} ∩ Y ∪ X_{2} ∩ Y and Y ∩ (X_{1} ∪ X_{2}) = Y ∩ X_{1} ∪ Y ∩ X_{2}.

(36) For every subspace Y of X such that X_{1} meets X_{2} holds X_{1} ∩ X_{2} ∪ Y = (X_{1} ∪ Y) ∩ (X_{2} ∪ Y) and Y ∪ X_{1} ∩ X_{2} = (Y ∪ X_{1}) ∩ (Y ∪ X_{2}).

3. Separated and weakly separated subsets of topological spaces

Let X be a topological space, and let A_{1}, A_{2} be subsets of X. Let us note that one can characterize the predicate A_{1} and A_{2} are separated by the following (equivalent) condition: (Def.6) \overline{A_{1}} ∩ A_{2} = ∅ and A_{1} ∩ \overline{A_{2}} = ∅.

In the sequel X is a topological space and A_{1}, A_{2} are subsets of X. We now state a number of propositions:

(37) If A_{1} and A_{2} are separated, then A_{1} misses A_{2}.

(38) If A_{1} is closed and A_{2} is closed, then A_{1} misses A_{2} if and only if A_{1} and A_{2} are separated.

(39) If A_{1} ∪ A_{2} is closed and A_{1} and A_{2} are separated, then A_{1} is closed and A_{2} is closed.

(40) If A_{1} misses A_{2}, then if A_{1} is open, then A_{1} misses \overline{A_{2}} but if A_{2} is open, then \overline{A_{1}} misses A_{2}.

(41) If A_{1} is open and A_{2} is open, then A_{1} misses A_{2} if and only if A_{1} and A_{2} are separated.

(42) If A_{1} ∪ A_{2} is open and A_{1} and A_{2} are separated, then A_{1} is open and A_{2} is open.

(43) For every subset C of X such that A_{1} and A_{2} are separated holds A_{1}∩C and A_{2} ∩ C are separated and C ∩ A_{1} and C ∩ A_{2} are separated.

(44) For every subset B of X holds if A_{1} and B are separated or A_{2} and B are separated, then A_{1} ∩ A_{2} and B are separated but if B and A_{1} are separated or B and A_{2} are separated, then B and A_{1} ∩ A_{2} are separated.

(45) For every subset B of X holds A_{1} and B are separated and A_{2} and B are separated if and only if A_{1} ∪ A_{2} and B are separated but B and A_{1} are separated and B and A_{2} are separated if and only if B and A_{1} ∪ A_{2} are separated.

(46) A_{1} and A_{2} are separated if and only if there exist subsets C_{1}, C_{2} of X such that A_{1} ⊆ C_{1} and A_{2} ⊆ C_{2} and C_{1} misses A_{2} and C_{2} misses A_{1} and C_{1} is closed and C_{2} is closed.

(47) A_{1} and A_{2} are separated if and only if there exist subsets C_{1}, C_{2} of X such that A_{1} ⊆ C_{1} and A_{2} ⊆ C_{2} and C_{1} ∩ C_{2} misses A_{1} ∪ A_{2} and C_{1} is closed and C_{2} is closed.

(48) A_{1} and A_{2} are separated if and only if there exist subsets C_{1}, C_{2} of X such that A_{1} ⊆ C_{1} and A_{2} ⊆ C_{2} and C_{1} misses A_{2} and C_{2} misses A_{1} and C_{1} is open and C_{2} is open.

(49) A_{1} and A_{2} are separated if and only if there exist subsets C_{1}, C_{2} of X such that A_{1} ⊆ C_{1} and A_{2} ⊆ C_{2} and C_{1} ∩ C_{2} misses A_{1} ∪ A_{2} and C_{1} is open and C_{2} is open.

Let X be a topological space, and let A_{1}, A_{2} be subsets of X. We say that A_{1} and A_{2} are weakly separated if and only if: (Def.7) A_{1} \ A_{2} and A_{2} \ A_{1} are separated.

In the sequel X will be a topological space and A_{1}, A_{2} will be subsets of X. We now state a number of propositions:

(50) If A_{1} and A_{2} are weakly separated, then A_{2} and A_{1} are weakly separated.

(51) A_{1} misses A_{2} and A_{1} and A_{2} are weakly separated if and only if A_{1} and A_{2} are separated.

(52) If A_{1} ⊆ A_{2} or A_{2} ⊆ A_{1}, then A_{1} and A_{2} are weakly separated.

(53) If A_{1} is closed and A_{2} is closed, then A_{1} and A_{2} are weakly separated.

(54) If A_{1} is open and A_{2} is open, then A_{1} and A_{2} are weakly separated.

(55) For every subset C of X such that A_{1} and A_{2} are weakly separated holds A_{1} ∪ C and A_{2} ∪ C are weakly separated and C ∪ A_{1} and C ∪ A_{2} are weakly separated.

(56) For all subsets B_{1}, B_{2} of X such that B_{1} ⊆ A_{2} and B_{2} ⊆ A_{1} holds if A_{1} and A_{2} are weakly separated, then A_{1} ∪ B_{1} and A_{2} ∪ B_{2} are weakly separated and B_{1} ∪ A_{1} and B_{2} ∪ A_{2} are weakly separated.

(57) For every subset B of X holds if A_{1} and B are weakly separated and A_{2} and B are weakly separated, then A_{1} ∩A_{2} and B are weakly separated but if B and A_{1} are weakly separated and B and A_{2} are weakly separated, then B and A_{1} ∩ A_{2} are weakly separated.

(58) For every subset B of X holds if A_{1} and B are weakly separated and A_{2} and B are weakly separated, then A_{1} ∪A_{2} and B are weakly separated but if B and A_{1} are weakly separated and B and A_{2} are weakly separated, then B and A_{1} ∪ A_{2} are weakly separated.

(59) A_{1} and A_{2} are weakly separated if and only if there exist subsets C_{1}, C_{2}, C of X such that C_{1} ∩ (A_{1} ∪ A_{2}) ⊆ A_{1} and C_{2} ∩ (A_{1} ∪ A_{2}) ⊆ A_{2} and C ∩ (A_{1} ∪ A_{2}) ⊆ A_{1} ∩ A_{2} and the carrier of X = C_{1} ∪ C_{2} ∪ C and C_{1} is closed and C_{2} is closed and C is open.

(60) Suppose A_{1} and A_{2} are weakly separated and A_{1} ⊈ A_{2} and A_{2} ⊈ A_{1}. Then there exist non-empty subsets C_{1}, C_{2} of X such that C_{1} is closed and C_{2} is closed and C_{1} ∩ (A_{1} ∪ A_{2}) ⊆ A_{1} and C_{2} ∩ (A_{1} ∪ A_{2}) ⊆ A_{2} but A_{1} ∪ A_{2} ⊆ C_{1} ∪ C_{2} or there exists a non-empty subset C of X such that C is open and C ∩ (A_{1} ∪ A_{2}) ⊆ A_{1} ∩ A_{2} and the carrier of X = C_{1} ∪ C_{2} ∪ C.

(61) If A_{1}∪A_{2} = the carrier of X, then A_{1} and A_{2} are weakly separated if and only if there exist subsets C_{1}, C_{2}, C of X such that A_{1} ∪A_{2} = C_{1} ∪C_{2} ∪C and C_{1} ⊆ A_{1} and C_{2} ⊆ A_{2} and C ⊆ A_{1} ∩ A_{2} and C_{1} is closed and C_{2} is closed and C is open.

(62) Suppose A_{1}∪A_{2} = the carrier of X and A_{1} and A_{2} are weakly separated and A_{1} ⊈ A_{2} and A_{2} ⊈ A_{1}. Then there exist non-empty subsets C_{1}, C_{2} of X such that C_{1} is closed and C_{2} is closed and C_{1} ⊆ A_{1} and C_{2} ⊆ A_{2} but A_{1} ∪ A_{2} = C_{1} ∪ C_{2} or there exists a non-empty subset C of X such that A_{1} ∪ A_{2} = C_{1} ∪ C_{2} ∪ C and C ⊆ A_{1} ∩ A_{2} and C is open.

(63) A_{1} and A_{2} are weakly separated if and only if there exist subsets C_{1}, C_{2}, C of X such that C_{1} ∩ (A_{1} ∪ A_{2}) ⊆ A_{1} and C_{2} ∩ (A_{1} ∪ A_{2}) ⊆ A_{2} and C ∩ (A_{1} ∪ A_{2}) ⊆ A_{1} ∩ A_{2} and the carrier of X = C_{1} ∪ C_{2} ∪ C and C_{1} is open and C_{2} is open and C is closed.

(64) Suppose A_{1} and A_{2} are weakly separated and A_{1} ⊈ A_{2} and A_{2} ⊈ A_{1}. Then there exist non-empty subsets C_{1}, C_{2} of X such that C_{1} is open and C_{2} is open and C_{1} ∩ (A_{1} ∪ A_{2}) ⊆ A_{1} and C_{2} ∩ (A_{1} ∪ A_{2}) ⊆ A_{2} but A_{1} ∪ A_{2} ⊆ C_{1} ∪ C_{2} or there exists a non-empty subset C of X such that C is closed and C ∩ (A_{1} ∪ A_{2}) ⊆ A_{1} ∩ A_{2} and the carrier of X = C_{1} ∪ C_{2} ∪ C.

(65) If A_{1}∪A_{2} = the carrier of X, then A_{1} and A_{2} are weakly separated if and only if there exist subsets C_{1}, C_{2}, C of X such that A_{1} ∪A_{2} = C_{1} ∪C_{2} ∪C and C_{1} ⊆ A_{1} and C_{2} ⊆ A_{2} and C ⊆ A_{1} ∩ A_{2} and C_{1} is open and C_{2} is open and C is closed.

(66) Suppose A_{1}∪A_{2} = the carrier of X and A_{1} and A_{2} are weakly separated and A_{1} ⊈ A_{2} and A_{2} ⊈ A_{1}. Then there exist non-empty subsets C_{1}, C_{2} of X such that C_{1} is open and C_{2} is open and C_{1} ⊆ A_{1} and C_{2} ⊆ A_{2} but A_{1} ∪ A_{2} = C_{1} ∪ C_{2} or there exists a non-empty subset C of X such that A_{1} ∪ A_{2} = C_{1} ∪ C_{2} ∪ C and C ⊆ A_{1} ∩ A_{2} and C is closed.

(67) A_{1} and A_{2} are separated if and only if there exist subsets B_{1}, B_{2} of X such that B_{1} and B_{2} are weakly separated and A_{1} ⊆ B_{1} and A_{2} ⊆ B_{2} and B_{1} ∩ B_{2} misses A_{1} ∪ A_{2}.

4. Separated and weakly separated subspaces of topological spaces

In the sequel X is a topological space. Let us consider X, and let X_{1}, X_{2} be subspaces of X. We say that X_{1} and X_{2} are separated if and only if: (Def.8) for all subsets A_{1}, A_{2} of X such that A_{1} = the carrier of X_{1} and

A_{2} = the carrier of X_{2} holds A_{1} and A_{2} are separated.

In the sequel X_{1}, X_{2} will denote subspaces of X. One can prove the following propositions:

(68) If X_{1} and X_{2} are separated, then X_{1} misses X_{2}.

(69) If X_{1} and X_{2} are separated, then X_{2} and X_{1} are separated.

(70) For all closed subspaces X_{1}, X_{2} of X holds X_{1} misses X_{2} if and only if X_{1} and X_{2} are separated.

(71) If X = X_{1} ∪ X_{2} and X_{1} and X_{2} are separated, then X_{1} is a closed subspace of X and X_{2} is a closed subspace of X.

(72) If X_{1} ∪X_{2} is a closed subspace of X and X_{1} and X_{2} are separated, then X_{1} is a closed subspace of X and X_{2} is a closed subspace of X.

(73) For all open subspaces X_{1}, X_{2} of X holds X_{1} misses X_{2} if and only if X_{1} and X_{2} are separated.

(74) If X = X_{1} ∪ X_{2} and X_{1} and X_{2} are separated, then X_{1} is an open subspace of X and X_{2} is an open subspace of X.

(75) If X_{1} ∪X_{2} is an open subspace of X and X_{1} and X_{2} are separated, then X_{1} is an open subspace of X and X_{2} is an open subspace of X.

(76) For all subspaces Y, X_{1}, X_{2} of X such that X_{1} meets Y and X_{2} meets Y holds if X_{1} and X_{2} are separated, then X_{1}∩Y and X_{2}∩Y are separated and Y ∩ X_{1} and Y ∩ X_{2} are separated.

(77) For all subspaces Y_{1}, Y_{2} of X such that Y_{1} is a subspace of X_{1} and Y_{2} is a subspace of X_{2} holds if X_{1} and X_{2} are separated, then Y_{1} and Y_{2} are separated.

(78) For every subspace Y of X such that X_{1} meets X_{2} holds if X_{1} and Y are separated or X_{2} and Y are separated, then X_{1} ∩ X_{2} and Y are separated but if Y and X_{1} are separated or Y and X_{2} are separated, then Y and X_{1} ∩ X_{2} are separated.

(79) For every subspace Y of X holds X_{1} and Y are separated and X_{2} and Y are separated if and only if X_{1} ∪ X_{2} and Y are separated but Y and X_{1} are separated and Y and X_{2} are separated if and only if Y and X_{1} ∪ X_{2} are separated.

(80) X_{1} and X_{2} are separated if and only if there exist closed subspaces Y_{1}, Y_{2} of X such that X_{1} is a subspace of Y_{1} and X_{2} is a subspace of Y_{2} and Y_{1} misses X_{2} and Y_{2} misses X_{1}.

(81) X_{1} and X_{2} are separated if and only if there exist closed subspaces Y_{1}, Y_{2} of X such that X_{1} is a subspace of Y_{1} and X_{2} is a subspace of Y_{2} but Y_{1} misses Y_{2} or Y_{1} ∩ Y_{2} misses X_{1} ∪ X_{2}.

(82) X_{1} and X_{2} are separated if and only if there exist open subspaces Y_{1}, Y_{2} of X such that X_{1} is a subspace of Y_{1} and X_{2} is a subspace of Y_{2} and Y_{1} misses X_{2} and Y_{2} misses X_{1}.

(83) X_{1} and X_{2} are separated if and only if there exist open subspaces Y_{1}, Y_{2} of X such that X_{1} is a subspace of Y_{1} and X_{2} is a subspace of Y_{2} but Y_{1} misses Y_{2} or Y_{1} ∩ Y_{2} misses X_{1} ∪ X_{2}.

Let X be a topological space, and let X_{1}, X_{2} be subspaces of X. We say that X_{1} and X_{2} are weakly separated if and only if:

(Def.9) for all subsets A_{1}, A_{2} of X such that A_{1} = the carrier of X_{1} and A_{2} = the carrier of X_{2} holds A_{1} and A_{2} are weakly separated.

In the sequel X_{1}, X_{2} will denote subspaces of X. The following propositions are true:

(84) If X_{1} and X_{2} are weakly separated, then X_{2} and X_{1} are weakly separated.

(85) X_{1} misses X_{2} and X_{1} and X_{2} are weakly separated if and only if X_{1} and X_{2} are separated.

(86) If X_{1} is a subspace of X_{2} or X_{2} is a subspace of X_{1}, then X_{1} and X_{2} are weakly separated.

(87) For all closed subspaces X_{1}, X_{2} of X holds X_{1} and X_{2} are weakly separated.

(88) For all open subspaces X_{1}, X_{2} of X holds X_{1} and X_{2} are weakly separated.

(89) For every subspace Y of X such that X_{1} and X_{2} are weakly separated holds X_{1} ∪ Y and X_{2} ∪ Y are weakly separated and Y ∪ X_{1} and Y ∪ X_{2} are weakly separated.

(90) For all subspaces Y_{1}, Y_{2} of X such that Y_{1} is a subspace of X_{2} and Y_{2} is a subspace of X_{1} holds if X_{1} and X_{2} are weakly separated, then X_{1} ∪ Y_{1} and X_{2} ∪ Y_{2} are weakly separated and Y_{1} ∪ X_{1} and Y_{2} ∪ X_{2} are weakly separated.

(91) For all subspaces Y, X_{1}, X_{2} of X such that X_{1} meets X_{2} holds if X_{1} and Y are weakly separated and X_{2} and Y are weakly separated, then X_{1}∩X_{2} and Y are weakly separated but if Y and X_{1} are weakly separated and Y and X_{2} are weakly separated, then Y and X_{1} ∩ X_{2} are weakly separated.

(92) For every subspace Y of X holds if X_{1} and Y are weakly separated and X_{2} and Y are weakly separated, then X_{1}∪X_{2} and Y are weakly separated but if Y and X_{1} are weakly separated and Y and X_{2} are weakly separated, then Y and X_{1} ∪ X_{2} are weakly separated.

(93) Let X be a strict topological space. Let X_{1}, X_{2} be subspaces of X. Suppose X_{1} meets X_{2}. Then X_{1} and X_{2} are weakly separated if and only if X_{1} is a subspace of X_{2} or X_{2} is a subspace of X_{1} or there exist closed subspaces Y_{1}, Y_{2} of X such that Y_{1} ∩ (X_{1} ∪ X_{2}) is a subspace of X_{1} and Y_{2} ∩ (X_{1} ∪ X_{2}) is a subspace of X_{2} but X_{1} ∪ X_{2} is a subspace of Y_{1} ∪ Y_{2} or there exists an open subspace Y of X such that X = Y_{1} ∪ Y_{2} ∪ Y and Y ∩ (X_{1} ∪ X_{2}) is a subspace of X_{1} ∩ X_{2}.

(94) Suppose X = X_{1} ∪ X_{2} and X_{1} meets X_{2}. Then X_{1} and X_{2} are weakly separated if and only if X_{1} is a subspace of X_{2} or X_{2} is a subspace of X_{1} or there exist closed subspaces Y_{1}, Y_{2} of X such that Y_{1} is a subspace of X_{1} and Y_{2} is a subspace of X_{2} but X = Y_{1} ∪ Y_{2} or there exists an open subspace Y of X such that X = Y_{1} ∪ Y_{2} ∪ Y and Y is a subspace of X_{1} ∩ X_{2}.

(95) If X = X_{1}∪X_{2} and X_{1} misses X_{2}, then X_{1} and X_{2} are weakly separated if and only if X_{1} is a closed subspace of X and X_{2} is a closed subspace of X.

(96) Let X be a strict topological space. Let X_{1}, X_{2} be subspaces of X. Suppose X_{1} meets X_{2}. Then X_{1} and X_{2} are weakly separated if and only if X_{1} is a subspace of X_{2} or X_{2} is a subspace of X_{1} or there exist open subspaces Y_{1}, Y_{2} of X such that Y_{1} ∩ (X_{1} ∪ X_{2}) is a subspace of X_{1} and Y_{2} ∩ (X_{1} ∪ X_{2}) is a subspace of X_{2} but X_{1} ∪ X_{2} is a subspace of Y_{1} ∪ Y_{2} or there exists a closed subspace Y of X such that X = Y_{1} ∪ Y_{2} ∪ Y and Y ∩ (X_{1} ∪ X_{2}) is a subspace of X_{1} ∩ X_{2}.

(97) Suppose X = X_{1} ∪ X_{2} and X_{1} meets X_{2}. Then X_{1} and X_{2} are weakly separated if and only if X_{1} is a subspace of X_{2} or X_{2} is a subspace of X_{1} or there exist open subspaces Y_{1}, Y_{2} of X such that Y_{1} is a subspace of X_{1} and Y_{2} is a subspace of X_{2} but X = Y_{1} ∪ Y_{2} or there exists a closed subspace Y of X such that X = Y_{1} ∪ Y_{2} ∪ Y and Y is a subspace of X_{1} ∩ X_{2}.

(98) If X = X_{1}∪X_{2} and X_{1} misses X_{2}, then X_{1} and X_{2} are weakly separated if and only if X_{1} is an open subspace of X and X_{2} is an open subspace of X.

(99) X_{1} and X_{2} are separated if and only if there exist subspaces Y_{1}, Y_{2} of X such that Y_{1} and Y_{2} are weakly separated and X_{1} is a subspace of Y_{1} and X_{2} is a subspace of Y_{2} but Y_{1} misses Y_{2} or Y_{1} ∩ Y_{2} misses X_{1} ∪ X_{2}.

674 zbigniew karno

Acknowledgements

I would like to express my gratitude to Professors A. Trybulec and C. Byliński for their valuable advice. I am also extremely grateful to W.A. Trybulec and to all participants of the Mizar Summer School (1991) for acquainting me with the Mizar system.

References

[1] Kazimierz Kuratowski. Topology. Volume I, PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.

[2] Beata Padlewska. Connected spaces. Formalized Mathematics, 1(1):239–244, 1990.

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

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

[5] Andrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4):535–545, 1991.

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

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

[8] Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231–237, 1990.

Received January 8, 1992

The de l’Hospital Theorem

Małgorzata Korolkiewicz Warsaw University Białystok

Summary. List of theorems concerning the de l’Hospital Theorem. We discuss the case when both functions have the zero value at a point and when the quotient of their differentials is convergent at this point.

MML Identifier: L'HOSPIT.

The papers [21], [4], [1], [2], [17], [15], [6], [9], [16], [3], [5], [12], [13], [20], [14], [18], [19], [8], [11], [7], and [10] provide the terminology and notation for this paper. We adopt the following rules: f, g will be partial functions from to , r, r_{1}, r_{2}, g_{1}, g_{2}, x_{0}, t will be real numbers, and a will be a sequence of real numbers. Next we state a number of propositions:

(1) If f is continuous in x_{0} and for all r_{1}, r_{2} such that r_{1} < x_{0} and x_{0} < r_{2} there exist g_{1}, g_{2} such that r_{1} < g_{1} and g_{1} < x_{0} and g_{1} ∈ dom f and g_{2} < r_{2} and x_{0} < g_{2} and g_{2} ∈ dom f, then f is convergent in x_{0}.

(2) f is right convergent in x_{0} and lim_{x_{0}}_{+} f = t if and only if the following conditions are satisfied:

(i) for every r such that x_{0} < r there exists t such that t < r and x_{0} < t and t ∈ dom f,

(ii) for every a such that a is convergent and lim a = x_{0} and rng a ⊆

dom f ∩]x_{0}, +∞[ holds f · a is convergent and lim(f · a) = t.

(3) f is left convergent in x_{0} and lim_{x_{0}}_{−} f = t if and only if the following conditions are satisfied:

(i) for every r such that r < x_{0} there exists t such that r < t and t < x_{0} and t ∈ dom f,

(ii) for every a such that a is convergent and lim a = x_{0} and rng a ⊆

dom f ∩]−∞, x_{0}[ holds f · a is convergent and lim(f · a) = t.

(4) Suppose There exists a neighbourhood N of x_{0} such that N \ {x_{0}} ⊆ dom f. Then for all r_{1}, r_{2} such that r_{1} < x_{0} and x_{0} < r_{2} there exist g_{1}, g_{2} such that r_{1} < g_{1} and g_{1} < x_{0} and g_{1} ∈ dom f and g_{2} < r_{2} and x_{0} < g_{2} and g_{2} ∈ dom f.

(5) Given a neighbourhood N of x_{0} such that

(i) f is differentiable on N, (ii) g is differentiable on N, (iii) N \ \{x_{0}\} ⊆ dom(\frac{f}{g}),

(iv) N ⊆ dom(\frac{f′_{N}}{g′_{N}} ),

(v) f(x_{0}) = 0, (vi) g(x_{0}) = 0, (vii) \frac{f′_{N}}{g′_{N}} is divergent to +∞ in x_{0}.

Then \frac{f}{g} is divergent to +∞ in x_{0}.

(6) Given a neighbourhood N of x_{0} such that

(i) f is differentiable on N, (ii) g is differentiable on N, (iii) N \ \{x_{0}\} ⊆ dom(\frac{f}{g}),

(iv) N ⊆ dom(\frac{f′_{N}}{g′_{N}} ),

(v) f(x_{0}) = 0, (vi) g(x_{0}) = 0, (vii) \frac{f′_{N}}{g′_{N}} is divergent to −∞ in x_{0}.

Then \frac{f}{g} is divergent to −∞ in x_{0}.

(7) Given r such that

(i) r > 0, (ii) f is differentiable on ]x_{0}, x_{0} + r[, (iii) g is differentiable on ]x_{0}, x_{0} + r[, (iv) ]x_{0}, x_{0} + r[ ⊆ dom(\frac{f}{g}),

(v) [x_{0}, x_{0} + r] ⊆ dom(\frac{f′_{]x_{0},x_{0}+r[}}{g′_{]x_{0},x_{0}+r[}} ),

(vi) f(x_{0}) = 0, (vii) g(x_{0}) = 0, (viii) f is continuous in x_{0}, (ix) g is continuous in x_{0},

(x) \frac{f′_{]x_{0},x_{0}+r[}}{g′_{]x_{0},x_{0}+r[}} is right convergent in x_{0}.

Then \frac{f}{g} is right convergent in x_{0} and there exists r such that r > 0 and

lim_{x_{0}}_{+}(\frac{f}{g}) = lim_{x_{0}}_{+}(\frac{f′_{]x_{0},x_{0}+r[}}{g′_{]x_{0},x_{0}+r[}} ).

(8) Given r such that

(i) r > 0, (ii) f is differentiable on ]x_{0} − r, x_{0}[, (iii) g is differentiable on ]x_{0} − r, x_{0}[, (iv) ]x_{0} − r, x_{0}[ ⊆ dom(\frac{f}{g}), (v) [x_{0} − r, x_{0}] ⊆ dom(\frac{f′_{]x_{0}−r,x_{0}[}}{g′_{]x_{0}−r,x_{0}[}} ),

(vi) f(x_{0}) = 0, (vii) g(x_{0}) = 0, (viii) f is continuous in x_{0}, (ix) g is continuous in x_{0},

(x) \frac{f′_{]x_{0}−r,x_{0}[}}{g′_{]x_{0}−r,x_{0}[}} is left convergent in x_{0}.

Then \frac{f}{g} is left convergent in x_{0} and there exists r such that r > 0 and

lim_{x_{0}}_{−}(\frac{f}{g}) = lim_{x_{0}}_{−}(\frac{f′_{]x_{0}−r,x_{0}[}}{g′_{]x_{0}−r,x_{0}[}} ).

(9) Given a neighbourhood N of x_{0} such that

(i) f is differentiable on N, (ii) g is differentiable on N, (iii) N \ \{x_{0}\} ⊆ dom(\frac{f}{g}),

(iv) N ⊆ dom(\frac{f′_{N}}{g′_{N}} ),

(v) f(x_{0}) = 0, (vi) g(x_{0}) = 0,

(vii) \frac{f′_{N}}{g′_{N}} is convergent in x_{0}.

Then \frac{f}{g} is convergent in x_{0} and there exists a neighbourhood N of x_{0} such

that lim_{x_{0}}(\frac{f}{g}) = lim_{x_{0}}(\frac{f′_{N}}{g′_{N}} ).

(10) Given a neighbourhood N of x_{0} such that (i) f is differentiable on N, (ii) g is differentiable on N, (iii) N \ \{x_{0}\} ⊆ dom(\frac{f}{g}),

(iv) N ⊆ dom(\frac{f′_{N}}{g′_{N}} ),

(v) f(x_{0}) = 0, (vi) g(x_{0}) = 0,

(vii) \frac{f′_{N}}{g′_{N}} is continuous in x_{0}.

Then \frac{f}{g} is convergent in x_{0} and lim_{x_{0}}(\frac{f}{g}) = \frac{f′(x_{0})}{g′(x_{0})}.

References

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

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

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

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

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

678 małgorzata korolkiewicz

[6] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273–275, 1990.

[7] Jarosław Kotowicz. The limit of a real function at a point. Formalized Mathematics, 2(1):71–80, 1991.

[8] Jarosław Kotowicz. The limit of a real function at infinity. Formalized Mathematics, 2(1):17–28, 1991.

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

[10] Jarosław Kotowicz. Monotonic and continuous real function. Formalized Mathematics, 2(3):403–405, 1991.

[11] Jarosław Kotowicz. One-side limits of a real function at a point. Formalized Mathematics, 2(1):29–40, 1991.

[12] Jarosław Kotowicz. Partial functions from a domain to a domain. Formalized Mathematics, 1(4):697–702, 1990.

[13] Jarosław Kotowicz. Partial functions from a domain to the set of real numbers. Formalized Mathematics, 1(4):703–709, 1990.

[14] Jarosław Kotowicz. Properties of real functions. Formalized Mathematics, 1(4):781–786, 1990.

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

[16] Andrzej Ne‘dzusiak. σ-fields and probability. Formalized Mathematics, 1(2):401–407, 1990.

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

[18] Konrad Raczkowski and Paweł Sadowski. Real function continuity. Formalized Mathematics, 1(4):787–791, 1990.

[19] Konrad Raczkowski and Paweł Sadowski. Real function differentiability. Formalized Mathematics, 1(4):797–801, 1990.

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

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

Comma Category

Grzegorz Bancerek Warsaw University, Białystok IM PAN, Warszawa Agata Darmochwał Warsaw University

Summary. Comma category of two functors is introduced.

MML Identifier: COMMACAT.

The terminology and notation used in this paper have been introduced in the following articles: [9], [10], [1], [5], [2], [7], [4], [3], [6], and [8]. We now define four new functors. Let x be arbitrary. The functor x_{1,1} is defined by: (Def.1) x_{1,1} = (x_{1})_{1}. The functor x_{1,2} is defined as follows: (Def.2) x_{1,2} = (x_{1})_{2}. The functor x_{2,1} is defined by: (Def.3) x_{2,1} = (x_{2})_{1}. The functor x_{2,2} is defined as follows: (Def.4) x_{2,2} = (x_{2})_{2}.

In the sequel x, x_{1}, x_{2}, y, y_{1}, y_{2} are arbitrary. One can prove the following proposition

(1) ⟨⟨⟨⟨x_{1}, x_{2}⟩⟩, y⟩⟩_{1,1} = x_{1} and ⟨⟨⟨⟨x_{1}, x_{2}⟩⟩, y⟩⟩_{1,2} = x_{2} and ⟨⟨x, ⟨⟨y_{1}, y_{2}⟩⟩⟩⟩_{2,1} = y_{1} and ⟨⟨x, ⟨⟨y_{1}, y_{2}⟩⟩⟩⟩_{2,2} = y_{2}.

Let D_{1}, D_{2}, D_{3} be non-empty sets, and let x be an element of [: [: D_{1}, D_{2} :], D_{3} :]. Then x_{1,1} is an element of D_{1}. Then x_{1,2} is an element of D_{2}.

Let D_{1}, D_{2}, D_{3} be non-empty sets, and let x be an element of [: D_{1}, [: D_{2}, D_{3} :] :]. Then x_{2,1} is an element of D_{2}. Then x_{2,2} is an element of D_{3}.

For simplicity we follow a convention: C, D, E are categories, c is an object of C, d is an object of D, x is arbitrary, f is a morphism of E, g is a morphism of C, h is a morphism of D, F is a functor from C to E, and G is a functor from D to E. Let us consider C, D, E, and let F be a functor from C to E, and let G be a functor from D to E. Let us assume that there exist c_{1}, d_{1}, f_{1} such that f_{1} ∈ hom(F (c_{1}), G(d_{1})). The functor Obj_{(F,G)} yields a non-empty subset of [: [: the objects of C, the objects of D:], the morphisms of E:] and is defined as follows: (Def.5) Obj_{(F,G)} = {⟨⟨⟨⟨c, d⟩⟩, f⟩⟩ : f ∈ hom(F (c), G(d))}.

In the sequel o, o_{1}, o_{2} will denote elements of Obj_{(F,G)}. The following proposition is true

(2) Suppose there exist c, d, f such that f ∈ hom(F (c), G(d)). Then o = ⟨⟨⟨⟨o_{1,1}, o_{1,2}⟩⟩, o_{2}⟩⟩ and o_{2} ∈ hom(F (o_{1,1}), G(o_{1,2})) and dom(o_{2}) = F (o_{1,1}) and cod(o_{2}) = G(o_{1,2}).

Let us consider C, D, E, F, G. Let us assume that there exist c_{1}, d_{1}, f_{1} such that f_{1} ∈ hom(F (c_{1}), G(d_{1})). The functor Morph_{(F,G)} yielding a non-empty subset of [: [: Obj_{(F,G)}, Obj_{(F,G)} qua a non-empty set :], [: the morphisms of C, the morphisms of D:] :] is defined by: (Def.6) Morph_{(F,G)} = {⟨⟨⟨⟨o_{1}, o_{2}⟩⟩, ⟨⟨g, h⟩⟩⟩⟩ : dom g = o_{1}_{1,1} ∧ cod g = o_{2}_{1,1} ∧

dom h = o_{1}_{1,2} ∧ cod h = o_{2}_{1,2} ∧ o_{2}_{2} · F (g) = G(h) · o_{1}_{2}}.

In the sequel k, k_{1}, k_{2}, k′ denote elements of Morph_{(F,G)}. Let us consider C, D, E, F, G, k. Then k_{1,1} is an element of Obj_{(F,G)}. Then k_{1,2} is an element of Obj_{(F,G)}. Then k_{2,1} is a morphism of C. Then k_{2,2} is a morphism of D.

The following proposition is true

(3) Suppose There exist c, d, f such that f ∈ hom(F (c), G(d)). Then

(i) k = ⟨⟨⟨⟨k_{1,1}, k_{1,2}⟩⟩, ⟨⟨k_{2,1}, k_{2,2}⟩⟩⟩⟩, (ii) dom(k_{2,1}) = (k_{1,1})_{1,1}, (iii) cod(k_{2,1}) = (k_{1,2})_{1,1}, (iv) dom(k_{2,2}) = (k_{1,1})_{1,2},

(v) cod(k_{2,2}) = (k_{1,2})_{1,2},

(vi) (k_{1,2})_{2} · F (k_{2,1}) = G(k_{2,2}) · (k_{1,1})_{2}.

Let us consider C, D, E, F, G, k_{1}, k_{2}. Let us assume that there exist c_{1}, d_{1}, f_{1} such that f_{1} ∈ hom(F (c_{1}), G(d_{1})). Let us assume that k_{1}_{1,2} = k_{2}_{1,1}. The functor k_{2} · k_{1} yielding an element of Morph_{(F,G)} is defined as follows: (Def.7) k_{2} · k_{1} = ⟨⟨⟨⟨k_{1}_{1,1}, k_{2}_{1,2}⟩⟩, ⟨⟨k_{2}_{2,1} · k_{1}_{2,1}, k_{2}_{2,2} · k_{1}_{2,2}⟩⟩⟩⟩.

Let us consider C, D, E, F, G. The functor ∘_{(F,G)} yields a partial function from [: Morph_{(F,G)}, Morph_{(F,G)} :] to Morph_{(F,G)} and is defined by: (Def.8) dom(∘_{(F,G)}) = {⟨⟨k_{1}, k_{2}⟩⟩ : k_{1}_{1,1} = k_{2}_{1,2}} and for all k, k′ such that ⟨⟨k,

k′⟩⟩ ∈ dom(∘_{(F,G)}) holds ∘_{(F,G)}(⟨⟨k, k′⟩⟩) = k · k′.

Let us consider C, D, E, F, G. Let us assume that there exist c_{1}, d_{1}, f_{1} such that f_{1} ∈ hom(F (c_{1}), G(d_{1})). The functor (F, G) yielding a strict category is defined by the conditions (Def.9). (Def.9) (i) The objects of (F, G) = Obj_{(F,G)},

(ii) the morphisms of (F, G) = Morph_{(F,G)}, (iii) for every k holds (the dom-map of (F, G))(k) = k_{1,1}, (iv) for every k holds (the cod-map of (F, G))(k) = k_{1,2},

(v) for every o holds (the id-map of (F, G))(o) = ⟨⟨⟨⟨o, o⟩⟩, ⟨⟨id_{(o1,1)}, id_{(o1,2)}⟩⟩⟩⟩,

comma category 681

(vi) the composition of (F, G) = ∘_{(F,G)}.

We now state two propositions:

(4) The objects of ˙ (x, y) = {x} and the morphisms of ˙ (x, y) = {y}.

(5) For all objects a, b of ˙ (x, y) holds hom(a, b) = {y}.

Let us consider C, c. The functor ˙ (c) yielding a strict subcategory of C is defined as follows:

(Def.10) ˙ (c) = ˙ (c, id_{c}).

We now define two new functors. Let us consider C, c. The functor (c, C) yields a strict category and is defined by:

(Def.11) (c, C) = ({_{}˙ (c) \atop ↪}, id_{C}).

The functor (C, c) yields a strict category and is defined as follows:

(Def.12) (C, c) = (id_{C}, {_{}˙ (c) \atop ↪}).

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

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

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

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

[8] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 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.

682

Context-Free Grammar - Part 1

Patricia L. Carlson Teachers’ College of English Białystok

Grzegorz Bancerek Warsaw University, Białystok IM PAN, Warsaw

Summary. The concept of context-free grammar and of derivability in grammar are introduced. Moreover, the language (set of finite sequences of symbols) generated by grammar and some grammars are defined. The notion convenient to prove facts on language generated by grammar with exchange of symbols on grammar of union and concatenation of languages is included.

MML Identifier: LANG1.

The notation and terminology used here have been introduced in the following papers: [9], [7], [1], [8], [10], [11], [4], [2], [6], [5], and [3]. We consider context-free grammars which are systems

⟨symbols, a initial symbol, rules⟩, where the symbols constitute a non-empty set, the initial symbol is an element of the symbols, and the rules constitute a relation between the symbols and (the symbols)^{∗}.

We now define two new modes. Let G be a context-free grammar. A symbol of G is an element of the symbols of G.

A string of G is an element of (the symbols of G)^{∗}.

Let D be a non-empty set, and let p, q be elements of D^{∗}. Then p^{}q is an element of D^{∗}.

Let D be a non-empty set. Then ε_{D} is an element of D^{∗}. Let d be an element of D. Then ⟨d⟩ is an element of D^{∗}. Let e be an element of D. Then ⟨d, e⟩ is an element of D^{∗}.

In the sequel G will denote a context-free grammar, s will denote a symbol of G, and n, m will denote strings of G. Let us consider G, s, n. The predicate s ⇒ n is defined as follows: (Def.1) ⟨⟨s, n⟩⟩ ∈ the rules of G.

We now define two new functors. Let us consider G. The terminals of G yields a set and is defined as follows:

(Def.2) the terminals of G = {s : ¬ ⋁_{n} s ⇒ n}. The nonterminals of G yielding a set is defined as follows: (Def.3) the nonterminals of G = {s : ⋁_{n} s ⇒ n}.

Next we state the proposition

(1) (The terminals of G) ∪ (the nonterminals of G) = the symbols of G. Let us consider G, n, m. The predicate n ⇒ m is defined by:

(Def.4) there exist strings n_{1}, n_{2}, n_{3} of G and there exists s such that n =

n_{1} ^{}⟨s⟩^{}n_{2} and m = n_{1} ^{}n_{3} ^{}n_{2} and s ⇒ n_{3}. In the sequel n_{1}, n_{2}, n_{3} denote strings of G. One can prove the following

four propositions:

(2) If s ⇒ n, then n_{1} ^{}⟨s⟩^{}n_{2} ⇒ n_{1} ^{}n^{}n_{2}.

(3) If s ⇒ n, then ⟨s⟩ ⇒ n.

(4) If ⟨s⟩ ⇒ n, then s ⇒ n.

(5) If n_{1} ⇒ n_{2}, then n^{}n_{1} ⇒ n^{}n_{2} and n_{1} ^{}n ⇒ n_{2} ^{}n. Let us consider G, n, m. The predicate n ⇒_{∗} m is defined by the condition

(Def.5). (Def.5) There exists a finite sequence p such that len p ≥ 1 and p(1) = n and

p(len p) = m and for every natural number i such that i ≥ 1 and i < len p there exist strings a, b of G such that p(i) = a and p(i+1) = b and a ⇒ b.

The following three propositions are true:

(6) n ⇒_{∗} n.

(7) If n ⇒ m, then n ⇒_{∗} m.

(8) If n_{2} ⇒_{∗} n_{1} and n_{3} ⇒_{∗} n_{2}, then n_{3} ⇒_{∗} n_{1}. Let us consider G. The language generated by G yielding a set is defined by:

(Def.6) the language generated by G = {a : rng a ⊆ the terminals of G ∧ ⟨the initial symbol of G⟩ ⇒_{∗} a}, where a ranges over elements of (the symbols of G)^{∗}.

Next we state the proposition

(9) n ∈ the language generated by G if and only if rng n ⊆ the terminals of G and ⟨the initial symbol of G⟩ ⇒_{∗} n.

Let a be arbitrary. Then {a} is a non-empty set. Let b be arbitrary. Then {a, b} is a non-empty set.

Let D, E be non-empty sets, and let a be an element of [: D, E:]. Then {a} is a relation between D and E. Let b be an element of [: D, E:]. Then {a, b} is a relation between D and E.

We now define three new functors. Let a be arbitrary. The functor {a ⇒ ε} yielding a strict context-free grammar is defined by: (Def.7) the symbols of {a ⇒ ε} = {a} and the rules of {a ⇒ ε} = {⟨⟨a, ε⟩⟩}.

Let b be arbitrary. The functor {a ⇒ b} yielding a strict context-free grammar is defined as follows: (Def.8) the symbols of {a ⇒ b} = {a, b} and the initial symbol of {a ⇒ b} = a

and the rules of {a ⇒ b} = {⟨⟨a, ⟨b⟩⟩⟩}.

The functor \{ \begin{matrix}a ⇒ ba \\ a ⇒ ε \end{matrix} \} yields a strict context-free grammar and is defined by:

(Def.9) the symbols of \{ \begin{matrix}a ⇒ ba \\ a ⇒ ε \end{matrix} \} = \{a, b\} and the initial symbol of \{ \begin{matrix}a ⇒ ba \\ a ⇒ ε \end{matrix} \} =

a and the rules of

\{ \begin{matrix}a ⇒ ba \\ a ⇒ ε \end{matrix} \} = \{⟨⟨a, ⟨b, a⟩⟩⟩, ⟨⟨a, ε⟩⟩\}.

Let D be a non-empty set. The total grammar over D yields a strict contextfree grammar and is defined as follows:

(Def.10) the symbols of the total grammar over D = D ∪ {D} and the initial symbol of the total grammar over D = D and the rules of the total grammar over D = {⟨⟨D, ⟨d, D⟩⟩⟩ : d = d} ∪ {⟨⟨D, ε⟩⟩}, where d ranges over elements of D.

In the sequel a, b are arbitrary and D denotes a non-empty set. Next we state several propositions:

(10) The terminals of {a ⇒ ε} = ∅.

(11) The language generated by {a ⇒ ε} = {ε}.

(12) If a ≠ b, then the terminals of {a ⇒ b} = {b}.

(13) If a ≠ b, then the language generated by {a ⇒ b} = {⟨b⟩}.

(14) If a ≠ b, then the terminals of \{ \begin{matrix}a ⇒ ba \\ a ⇒ ε \end{matrix} \} = \{b\}.

(15) If a ≠ b, then the language generated by \{ \begin{matrix}a ⇒ ba \\ a ⇒ ε \end{matrix} \} = \{b\}^{∗}.

(16) The terminals of the total grammar over D = D.

(17) The language generated by the total grammar over D = D^{∗}.

We now define two new attributes. A context-free grammar is efective if: (Def.11) the language generated by it is non-empty and the initial symbol of

it ∈ the nonterminals of it and for every symbol s of it such that s ∈ the terminals of it there exists a string p of it such that p ∈ the language generated by it and s ∈ rng p.

A context-free grammar is finite if: (Def.12) the rules of it is finite.

Let G be an efective context-free grammar. Then the nonterminals of G is a non-empty subset of the symbols of G.

Let X be a set, and let Y be a non-empty set, and let f be a function from X into Y. Then graph f is a relation between X and Y.

Let X, Y be non-empty sets, and let p be a finite sequence of elements of X, and let f be a function from X into Y. Then f · p is an element of Y^{∗}.

Let X, Y be non-empty sets, and let f be a function from X into Y. The functor f^{∗} yielding a function from X^{∗} into Y^{∗} is defined as follows:

(Def.13) for every element p of X^{∗} holds f^{∗}(p) = f · p.

Let R be a binary relation. The functor R^{∗} yielding a binary relation is defined by the condition (Def.14).

(Def.14) Let x, y be arbitrary. Then ⟨⟨x, y⟩⟩ ∈ R^{∗} if and only if the following

conditions are satisfied:

(i) x ∈ field R, (ii) y ∈ field R, (iii) there exists a finite sequence p such that len p ≥ 1 and p(1) = x and

p(len p) = y and for every natural number i such that i ≥ 1 and i < len p holds ⟨⟨p(i), p(i + 1)⟩⟩ ∈ R.

In the sequel R is a binary relation. We now state the proposition

(18) R ⊆ R^{∗}.

Let X be a non-empty set, and let R be a binary relation on X. Then R^{∗} is a binary relation on X.

Let G be a context-free grammar, and let X be a non-empty set, and let f be a function from the symbols of G into X. The functor G(f) yielding a strict context-free grammar is defined by:

(Def.15) G(f) = ⟨X, f(the initial symbol of G), (graph f)^{}· the rules of G · graph(f^{∗})⟩.

The following proposition is true

(19) For all non-empty sets D_{1}, D_{2} such that D_{1} ⊆ D_{2} holds D_{1}^{∗} ⊆ D_{2}^{∗}.

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. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990.

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

[5] Czesław Byliński. 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] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

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

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

context-free grammar - part 1 687

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

1990.

Received February 21, 1992 688

Completeness of the σ-Additive Measure. Measure Theory

Józef Białas University of Łódź

Summary. Definitions and basic properties of a σ-additive, nonnegative measure, with values in \overline{}, the enlarged set of real numbers, where \overline{}denotes set \overline{}= ∪ \{−∞, +∞\} - by [13]. The article includs the text being a continuation of the paper [5]. Some theorems concerning basic properties of a σ-additive measure and completeness of the measure are proved.

MML Identifier: MEASURE3.

The papers [15], [14], [9], [10], [7], [8], [1], [12], [2], [11], [3], [4], [6], and [5] provide the terminology and notation for this paper. One can prove the following four propositions:

(1) For every Real number x such that −∞ < x and x < +∞ holds x is a real number.

(2) For every Real number x such that x ≠ −∞ and x ≠ +∞ holds x is a real number.

(3) For all functions F_{1}, F_{2} from into \overline{}such that F_{1} is non-negative and F_{2} is non-negative holds if for every natural number n holds (Ser F_{1})(n) ≤ (Ser F_{2})(n), then ∑ F_{1} ≤ ∑ F_{2}.

(4) For all functions F_{1}, F_{2} from into \overline{}such that F_{1} is non-negative and F_{2} is non-negative holds if for every natural number n holds (Ser F_{1})(n) = (Ser F_{2})(n), then ∑ F_{1} = ∑ F_{2}.

Let X be a set, and let S be a σ-field of subsets of X. A denumerable family of subsets of X is called a subfamily of S if: (Def.1) it ⊆ S.

Let X be a set, and let S be a σ-field of subsets of X, and let F be a function from into S. Then rng F is a subfamily of S.

Let X be a set, and let S be a σ-field of subsets of X, and let A be a subfamily of S. Then ⋃ A is an element of S.

Let X be a set, and let S be a σ-field of subsets of X, and let A be a subfamily of S. Then ⋂ A is an element of S.

One can prove the following propositions:

(5) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S and for every function F from into S and for every element A of S such that ⋂ rng F ⊆ A and for every element n of holds A ⊆ F (n) holds M(A) = M(⋂ rng F).

(6) Let X be a set. Let S be a σ-field of subsets of X. Let G be a function from into S. Then for every function F from into S such that G(0) = ∅ and for every element n of holds G(n + 1) = F (0) \ F (n) and F (n + 1) ⊆ F (n) holds ⋃ rng G = F (0) \ ⋂ rng F.

(7) Let X be a set. Let S be a σ-field of subsets of X. Let G be a function from into S. Then for every function F from into S such that G(0) = ∅ and for every element n of holds G(n + 1) = F (0) \ F (n) and F (n + 1) ⊆ F (n) holds ⋂ rng F = F (0) \ ⋃ rng G.

(8) Let X be a set. Let S be a σ-field of subsets of X. Let M be a σmeasure on S. Let G be a function from into S. Let F be a function from into S. Suppose M(F (0)) < +∞ and G(0) = ∅ and for every element n of holds G(n + 1) = F (0) \ F (n) and F (n + 1) ⊆ F (n). Then M(⋂ rng F) = M(F (0)) − M(⋃ rng G).

(9) Let X be a set. Let S be a σ-field of subsets of X. Let M be a σmeasure on S. Let G be a function from into S. Let F be a function from into S. Suppose M(F (0)) < +∞ and G(0) = ∅ and for every element n of holds G(n + 1) = F (0) \ F (n) and F (n + 1) ⊆ F (n). Then M(⋃ rng G) = M(F (0)) − M(⋂ rng F).

(10) Let X be a set. Let S be a σ-field of subsets of X. Let M be a σmeasure on S. Let G be a function from into S. Let F be a function from into S. Suppose M(F (0)) < +∞ and G(0) = ∅ and for every element n of holds G(n + 1) = F (0) \ F (n) and F (n + 1) ⊆ F (n). Then M(⋂ rng F) = M(F (0)) − sup rng(M · G).

(11) Let X be a set. Let S be a σ-field of subsets of X. Let M be a σmeasure on S. Let G be a function from into S. Let F be a function from into S. Suppose M(F (0)) < +∞ and G(0) = ∅ and for every element n of holds G(n + 1) = F (0) \ F (n) and F (n + 1) ⊆ F (n). Then sup rng(M · G) is a real number and M(F (0)) is a real number and inf rng(M · F) is a real number.

(12) Let X be a set. Let S be a σ-field of subsets of X. Let M be a σmeasure on S. Let G be a function from into S. Let F be a function from into S. Suppose M(F (0)) < +∞ and G(0) = ∅ and for every element n of holds G(n + 1) = F (0) \ F (n) and F (n + 1) ⊆ F (n). Then sup rng(M · G) = M(F (0)) − inf rng(M · F).

completeness of the σ-additive … 691

(13) Let X be a set. Let S be a σ-field of subsets of X. Let M be a σmeasure on S. Let G be a function from into S. Let F be a function from into S. Suppose M(F (0)) < +∞ and G(0) = ∅ and for every element n of holds G(n + 1) = F (0) \ F (n) and F (n + 1) ⊆ F (n). Then inf rng(M · F) = M(F (0)) − sup rng(M · G).

(14) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S and for every function F from into S such that for every element n of holds F (n + 1) ⊆ F (n) and M(F (0)) < +∞ holds M(⋂ rng F) = inf rng(M · F).

(15) For every set X and for every σ-field S of subsets of X and for every measure M on S and for every family T of measureable sets of S and for every sequence F of separated subsets of S such that T = rng F holds ∑(M · F) ≤ M(⋃ T).

(16) For every set X and for every σ-field S of subsets of X and for every measure M on S and for every sequence F of separated subsets of S holds ∑(M · F) ≤ M(⋃ rng F).

(17) For every set X and for every σ-field S of subsets of X and for every measure M on S such that for every sequence F of separated subsets of S holds M(⋃ rng F) ≤ ∑(M · F) holds M is a σ-measure on S.

Let X be a set, and let S be a σ-field of subsets of X, and let M be a σ-measure on S. We say that M is complete on S if and only if: (Def.2) for every subset A of X and for every set B such that B ∈ S holds if

A ⊆ B and M(B) = 0\overline{}, then A ∈ S.

Let X be a set, and let S be a σ-field of subsets of X, and let M be a σ-measure on S. A subset of X is called a set with measure zero w.r.t. M if: (Def.3) there exists a set B such that B ∈ S and it ⊆ B and M(B) = 0\overline{}.

Let X be a set, and let S be a σ-field of subsets of X, and let M be a σmeasure on S. The functor COM(S, M) yielding a non-empty family of subsets of X is defined as follows: (Def.4) for an arbitrary A holds A ∈ COM(S, M) if and only if there exists a

set B such that B ∈ S and there exists a set C with measure zero w.r.t. M such that A = B ∪ C.

Let X be a set, and let S be a σ-field of subsets of X, and let M be a σmeasure on S, and let A be an element of COM(S, M). The functor MeasPartA yields a non-empty family of subsets of X and is defined as follows: (Def.5) for an arbitrary B holds B ∈ MeasPartA if and only if B ∈ S and

B ⊆ A and A \ B is a set with measure zero w.r.t. M.

Let X be a set, and let S be a σ-field of subsets of X, and let M be a σmeasure on S, and let F be a function from into COM(S, M), and let n be a natural number. Then F (n) is an element of COM(S, M).

We now state four propositions:

(18) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S and for every function F from into COM(S, M) there exists a function G from into S such that for every element n of holds G(n) ∈ MeasPartF (n).

(19) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S and for every function F from into COM(S, M) and for every function G from into S there exists a function H from into 2^{X} such that for every element n of holds H(n) = F (n) \ G(n).

(20) Let X be a set. Then for every σ-field S of subsets of X and for every σ-measure M on S and for every function F from into 2^{X} such that for every element n of holds F (n) is a set with measure zero w.r.t. M there exists a function G from into S such that for every element n of holds F (n) ⊆ G(n) and M(G(n)) = 0\overline{}.

(21) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S and for every non-empty family D of subsets of X such that for an arbitrary A holds A ∈ D if and only if there exists a set B such that B ∈ S and there exists a set C with measure zero w.r.t. M such that A = B ∪ C holds D is a σ-field of subsets of X.

Let X be a set, and let S be a σ-field of subsets of X, and let M be a σ-measure on S. Then COM(S, M) is a σ-field of subsets of X.

Next we state the proposition

(22) For every set X and for every σ-field S of subsets of X and for every σmeasure M on S and for all sets B_{1}, B_{2} such that B_{1} ∈ S and B_{2} ∈ S and for all sets C_{1}, C_{2} with measure zero w.r.t. M such that B_{1}∪C_{1} = B_{2}∪C_{2} holds M(B_{1}) = M(B_{2}).

Let X be a set, and let S be a σ-field of subsets of X, and let M be a σmeasure on S. The functor COM(M) yields a σ-measure on COM(S, M) and is defined by: (Def.6) for every set B such that B ∈ S and for every set C with measure zero

w.r.t. M holds (COM(M))(B ∪ C) = M(B).

The following proposition is true

(23) For every set X and for every σ-field S of subsets of X and for every σ-measure M on S holds COM(M) is complete on COM(S, M).

References

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

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

[3] Józef Białas. Infimum and supremum of the set of real numbers. Measure theory. Formalized Mathematics, 2(1):163–171, 1991.

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

[5] Józef Białas. Several properties of the σ-additive measure. Formalized Mathematics, 2(4):493–497, 1991.

completeness of the σ-additive … 693

[6] Józef Białas. The σ-additive measure theory. Formalized Mathematics, 2(2):263–270, 1991.

[7] Czesław Byliński. Basic functions and operations on functions. Formalized Mathematics, 1(1):245–254, 1990.

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

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

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

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

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

[13] R. Sikorski. Rachunek różniczkowy i całkowy - funkcje wielu zmiennych. Biblioteka Matematyczna, PWN - Warszawa, 1968.

[14] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

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

694

Series in Banach and Hilbert Spaces

Elżbieta Kraszewska Warsaw University Białystok

Jan Popiołek Warsaw University Białystok

Summary. In [20] the series of real numbers were investigated. The introduction to Banach and Hilbert Spaces ( [12,13,14]), enables us to arrive at the concept of series in Hilbert Space. We start with the notions: partial sums of series, sum and n-th sum of series, convergent series (summable series), absolutely convergent series. We prove some basic theorems: the necessary condition for a series to converge, Weierstrass’ test, d’Alembert’s test, Cauchy’s test.

MML Identifier: BHSP 4.

The notation and terminology used here have been introduced in the following articles: [5], [23], [28], [3], [4], [1], [10], [8], [9], [7], [20], [2], [29], [21], [22], [17], [27], [26], [24], [16], [12], [13], [15], [6], [11], [14], [25], [18], and [19]. For simplicity we adopt the following convention: X denotes a real unitary space, a, b, r denote real numbers, s_{1}, s_{2}, s_{3} denote sequences of X, R_{1}, R_{2}, R_{3} denote sequences of real numbers, and k, n, m denote natural numbers. The scheme Rec Func Ex RUS deals with a real unitary space A, a point B of A, and a binary functor F yielding a point of A and states that:

there exists a function f from into the vectors of the vectors of A such that f(0) = B and for every element n of and for every point x of A such that x = f(n) holds f(n + 1) = F(n, x) for all values of the parameters.

Let us consider X, s_{1}. The functor (∑_{α=0}^{κ} s_{1}(α))_{κ∈} yields a sequence of X and is defined as follows: (Def.1) (∑_{α=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). Next we state several propositions:

(1) (∑_{α=0}^{κ} s_{2}(α))_{κ∈} + (∑_{α=0}^{κ} s_{3}(α))_{κ∈} = (∑_{α=0}^{κ}(s_{2} + s_{3})(α))_{κ∈} .

(2) (∑_{α=0}^{κ} s_{2}(α))_{κ∈} − (∑_{α=0}^{κ} s_{3}(α))_{κ∈} = (∑_{α=0}^{κ}(s_{2} − s_{3})(α))_{κ∈} .

(3) (∑_{α=0}^{κ}(a · s_{1})(α))_{κ∈} = a · (∑_{α=0}^{κ} s_{1}(α))_{κ∈} .

(4) (∑_{α=0}^{κ}(−s_{1})(α))_{κ∈} = −(∑_{α=0}^{κ} s_{1}(α))_{κ∈} .

(5) a·(∑_{α=0}^{κ} s_{2}(α))_{κ∈} +b·(∑_{α=0}^{κ} s_{3}(α))_{κ∈} = (∑_{α=0}^{κ}(a·s_{2} +b·s_{3})(α))_{κ∈} . Let us consider X, s_{1}. We say that s_{1} is summable if and only if:

(Def.2) (∑_{α=0}^{κ} s_{1}(α))_{κ∈} is convergent.

Let us consider X, s_{1}. Let us assume that s_{1} is summable. The functor ∑ s_{1} yielding a point of X is defined by: (Def.3) ∑ s_{1} = lim((∑_{α=0}^{κ} s_{1}(α))_{κ∈} ).

Next we state several propositions:

(6) 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}.

(7) 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}.

(8) If s_{1} is summable, then a · s_{1} is summable and ∑(a · s_{1}) = a · ∑ s_{1}.

(9) If s_{1} is summable, then s_{1} is convergent and lim s_{1} = 0_{the vectors of X}.

(10) If X is a Hilbert space, then s_{1} is summable if and only if for every r such that r > 0 there exists k such that for all n, m such that n ≥ k and m ≥ k holds ∥(∑_{α=0}^{κ} s_{1}(α))_{κ∈} (n) − (∑_{α=0}^{κ} s_{1}(α))_{κ∈} (m)∥ < r.

(11) If s_{1} is summable, then (∑_{α=0}^{κ} s_{1}(α))_{κ∈} is bounded.

(12) For all s_{1}, s_{2} such that for every n holds s_{2}(n) = s_{1}(0) holds (∑_{α=0}^{κ}(s_{1} ↑ 1)(α))_{κ∈} = (∑_{α=0}^{κ} s_{1}(α))_{κ∈} ↑ 1 − s_{2}.

(13) If s_{1} is summable, then for every k holds s_{1} ↑ k is summable.

(14) If there exists k such that s_{1} ↑ k is summable, then s_{1} is summable. Let us consider X, s_{1}, n. The functor ∑_{κ=0}^{n} s_{1}(κ) yielding a point of X is

defined by: (Def.4) ∑_{κ=0}^{n} s_{1}(κ) = (∑_{α=0}^{κ} s_{1}(α))_{κ∈} (n).

We now state several propositions:

(15) ∑_{κ=0}^{n} s_{1}(κ) = (∑_{α=0}^{κ} s_{1}(α))_{κ∈} (n).

(16) ∑_{κ=0}^{0} s_{1}(κ) = s_{1}(0).

(17) ∑_{κ=0}^{1} s_{1}(κ) = ∑_{κ=0}^{0} s_{1}(κ) + s_{1}(1).

(18) ∑_{κ=0}^{1} s_{1}(κ) = s_{1}(0) + s_{1}(1).

(19) ∑_{κ=0}^{n+1} s_{1}(κ) = ∑_{κ=0}^{n} s_{1}(κ) + s_{1}(n + 1).

(20) s_{1}(n + 1) = ∑_{κ=0}^{n+1} s_{1}(κ) − ∑_{κ=0}^{n} s_{1}(κ).

(21) s_{1}(1) = ∑_{κ=0}^{1} s_{1}(κ) − ∑_{κ=0}^{0} s_{1}(κ).

Let us consider X, s_{1}, n, m. The functor ∑_{κ=n+1}^{m} s_{1}(κ) yielding a point of X is defined by: (Def.5) ∑_{κ=n+1}^{m} s_{1}(κ) = ∑_{κ=0}^{n} s_{1}(κ) − ∑_{κ=0}^{m} s_{1}(κ).

The following propositions are true:

(22) ∑_{κ=n+1}^{m} s_{1}(κ) = ∑_{κ=0}^{n} s_{1}(κ) − ∑_{κ=0}^{m} s_{1}(κ).

(23) ∑_{κ=1+1}^{0} s_{1}(κ) = s_{1}(1).

(24) ∑_{κ=n+1+1}^{n} s_{1}(κ) = s_{1}(n + 1).

(25) If X is a Hilbert space, then s_{1} is summable if and only if for every r such that r > 0 there exists k such that for all n, m such that n ≥ k and m ≥ k holds ∥∑_{κ=0}^{n} s_{1}(κ) − ∑_{κ=0}^{m} s_{1}(κ)∥ < r.

(26) If X is a Hilbert space, then s_{1} is summable if and only if for every r such that r > 0 there exists k such that for all n, m such that n ≥ k and m ≥ k holds ∥∑_{κ=n+1}^{m} s_{1}(κ)∥ < r.

Let us consider R_{1}, n. The functor ∑_{κ=0}^{n} R_{1}(κ) yields a real number and is defined by: (Def.6) ∑_{κ=0}^{n} R_{1}(κ) = (∑_{α=0}^{κ} R_{1}(α))_{κ∈} (n).

Let us consider R_{1}, n, m. The functor ∑_{κ=n+1}^{m} R_{1}(κ) yielding a real number is defined by: (Def.7) ∑_{κ=n+1}^{m} R_{1}(κ) = ∑_{κ=0}^{n} R_{1}(κ) − ∑_{κ=0}^{m} R_{1}(κ).

Let us consider X, s_{1}. We say that s_{1} is absolutely summable if and only if: (Def.8) ∥s_{1}∥ is summable.

The following propositions are true:

(27) If s_{2} is absolutely summable and s_{3} is absolutely summable, then s_{2}+s_{3} is absolutely summable.

(28) If s_{1} is absolutely summable, then a · s_{1} is absolutely summable.

(29) If for every n holds ∥s_{1}∥(n) ≤ R_{1}(n) and R_{1} is summable, then s_{1} is absolutely summable.

(30) If for every n holds s_{1}(n) ≠ 0_{the vectors of X} and R_{1}(n) = \frac{∥s_{1}(n+1)∥}{∥s_{1}(n)∥} and R_{1} is convergent and lim R_{1} < 1, then s_{1} is absolutely summable.

(31) 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_{the vectors of X}.

(32) If for every n holds s_{1}(n) ≠ 0_{the vectors of X} 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 summable.

(33) If for every n holds s_{1}(n) ≠ 0_{the vectors of X} and for every n holds R_{1}(n) = \frac{∥s_{1}(n+1)∥}{∥s_{1}(n)∥} and R_{1} is convergent and lim R_{1} > 1, then s_{1} is not summable.

(34) If for every n holds R_{1}(n) = ^{n} \sqrt{∥s_{1}(n)∥} and R_{1} is convergent and lim R_{1} < 1, then s_{1} is absolutely summable.

(35) If for every n holds R_{1}(n) = ^{n} \sqrt{∥s_{1}∥(n)} and there exists m such that for every n such that n ≥ m holds R_{1}(n) ≥ 1, then s_{1} is not summable.

(36) If for every n holds R_{1}(n) = ^{n} \sqrt{∥s_{1}∥(n)} and R_{1} is convergent and lim R_{1} > 1, then s_{1} is not summable.

(37) (∑_{α=0}^{κ}∥s_{1}∥(α))_{κ∈} is non-decreasing.

(38) For every n holds (∑_{α=0}^{κ}∥s_{1}∥(α))_{κ∈} (n) ≥ 0.

(39) For every n holds ∥(∑_{α=0}^{κ} s_{1}(α))_{κ∈} (n)∥ ≤ (∑_{α=0}^{κ}∥s_{1}∥(α))_{κ∈} (n).

(40) For every n holds ∥∑_{κ=0}^{n} s_{1}(κ)∥ ≤ ∑_{κ=0}^{n}∥s_{1}∥(κ).

(41) For all n, m holds ∥(∑_{α=0}^{κ} s_{1}(α))_{κ∈} (m) − (∑_{α=0}^{κ} s_{1}(α))_{κ∈} (n)∥ ≤ |(∑_{α=0}^{κ}∥s_{1}∥(α))_{κ∈} (m) − (∑_{α=0}^{κ}∥s_{1}∥(α))_{κ∈} (n)|.

(42) For all n, m holds ∥∑_{κ=0}^{m} s_{1}(κ) − ∑_{κ=0}^{n} s_{1}(κ)∥ ≤ | ∑_{κ=0}^{m}∥s_{1}∥(κ) − ∑_{κ=0}^{n}∥s_{1}∥(κ)|.

(43) For all n, m holds ∥∑_{κ=m+1}^{n} s_{1}(κ)∥ ≤ | ∑_{κ=m+1}^{n}∥s_{1}∥(κ)|.

(44) If X is a Hilbert space, then if s_{1} is absolutely summable, then s_{1} is

summable. Let us consider X, s_{1}, R_{1}. The functor R_{1} · s_{1} yielding a sequence of X is

defined as follows: (Def.9) for every n holds (R_{1} · s_{1})(n) = R_{1}(n) · s_{1}(n).

One can prove the following propositions:

(45) R_{1} · (s_{2} + s_{3}) = R_{1} · s_{2} + R_{1} · s_{3}.

(46) (R_{2} + R_{3}) · s_{1} = R_{2} · s_{1} + R_{3} · s_{1}.

(47) (R_{2} R_{3}) · s_{1} = R_{2} · (R_{3} · s_{1}).

(48) (a R_{1}) · s_{1} = a · (R_{1} · s_{1}).

(49) R_{1} · −s_{1} = (−R_{1}) · s_{1}.

(50) If R_{1} is convergent and s_{1} is convergent, then R_{1} · s_{1} is convergent.

(51) If R_{1} is bounded and s_{1} is bounded, then R_{1} · s_{1} is bounded.

(52) If R_{1} is convergent and s_{1} is convergent, then R_{1} · s_{1} is convergent and

lim(R_{1} · s_{1}) = lim R_{1} · lim s_{1}. Let us consider R_{1}. We say that R_{1} is a Cauchy sequence if and only if:

(Def.10) for every r such that r > 0 there exists k such that for all n, m such

that n ≥ k and m ≥ k holds |R_{1}(n) − R_{1}(m)| < r. One can prove the following propositions:

(53) If X is a Hilbert space, then if s_{1} is a Cauchy sequence and R_{1} is a Cauchy sequence, then R_{1} · s_{1} is a Cauchy sequence.

(54) For every n holds (∑_{α=0}^{κ}((R_{1} − R_{1} ↑ 1) · (∑_{α=0}^{κ} s_{1}(α))_{κ∈} )(α))_{κ∈} (n) = (∑_{α=0}^{κ}(R_{1} · s_{1})(α))_{κ∈} (n + 1) − (R_{1} · (∑_{α=0}^{κ} s_{1}(α))_{κ∈} )(n + 1).

(55) For every n holds (∑_{α=0}^{κ}(R_{1}·s_{1})(α))_{κ∈} (n+1) = (R_{1}·(∑_{α=0}^{κ} s_{1}(α))_{κ∈} )(n+1)−(∑_{α=0}^{κ}((R_{1}↑ 1 − R_{1}) · (∑_{α=0}^{κ} s_{1}(α))_{κ∈} )(α))_{κ∈} (n).

(56) For every n holds ∑_{κ=0}^{n+1}(R_{1} · s_{1})(κ) = (R_{1} · (∑_{α=0}^{κ} s_{1}(α))_{κ∈} )(n + 1) − ∑_{κ=0}^{n}((R_{1} ↑ 1 − R_{1}) · (∑_{α=0}^{κ} s_{1}(α))_{κ∈} )(κ).

References

[1] Czesław Byliński. Basic functions and operations on functions. Formalized Mathematics, 1(1):245–254, 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,

series in banach and hilbert spaces 699

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

[6] Krzysztof Hryniewiecki. Recursive definitions. Formalized Mathematics, 1(2):321–328, 1990.

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

[8] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273–275, 1990.

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

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

[11] Andrzej Ne‘dzusiak. Probability. Formalized Mathematics, 1(4):745–749, 1990.

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

[13] Jan Popiołek. Introduction to Banach and Hilbert spaces - part II. Formalized Mathematics, 2(4):517–521, 1991.

[14] Jan Popiołek. Introduction to Banach and Hilbert spaces - part III. Formalized Mathematics, 2(4):523–526, 1991.

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

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

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

[18] Konrad Raczkowski. Integer and rational exponents. Formalized Mathematics, 2(1):125– 130, 1991.

[19] Konrad Raczkowski and Andrzej Ne‘dzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213–216, 1991.

[20] Konrad Raczkowski and Andrzej Ne‘dzusiak. Serieses. Formalized Mathematics, 2(4):449–452, 1991.

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

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

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

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

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

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

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

[28] Zinaida Trybulec and Halina Świe‘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.

Received April 1, 1992 700

Products and Coproducts in Categories

Czesław Byliński Warsaw University Białystok

Summary. A product and coproduct in categories are introduced. The concepts included corresponds to that presented in [7].

MML Identifier: CAT 3.

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

1. Indexed families

For simplicity we adopt the following rules: I will be a set, x, x_{1}, x_{2}, y, y_{1}, y_{2} will be arbitrary, A will be a non-empty set, C, D will be categories, a, b, c, d will be objects of C, and f, g, h, k, p_{1}, p_{2}, q_{1}, q_{2}, i_{1}, i_{2}, j_{1}, j_{2} will be morphisms of C. Let us consider I, x, A, and let F be a function from I into A. Let us assume that x ∈ I. The functor F_{x} yielding an element of A is defined as follows:

(Def.1) F_{x} = F (x).

The scheme LambdaIdx deals with a set A, a set B, and a unary functor F yielding an element of B and states that:

there exists a function F from A into B such that for every x such that x ∈ A holds F_{x} = F(x) for all values of the parameters.

The following proposition is true

(1) For all functions F_{1}, F_{2} from I into A such that for every x such that x ∈ I holds F_{1}_{x} = F_{2}_{x} holds F_{1} = F_{2}.

The scheme FuncIdx correctn deals with a set A, a set B, and a unary functor F yielding an element of B and states that:

(i) there exists a function F from A into B such that for every x such that x ∈ A holds F_{x} = F(x), (ii) for all functions F_{1}, F_{2} from A into B such that for every x such that x ∈ A holds F_{1}_{x} = F(x) and for every x such that x ∈ A holds F_{2}_{x} = F(x) holds F_{1} = F_{2} for all values of the parameters.

Let us consider A, I, and let a be an element of A. Then I ⟼ a is a function from I into A.

The following proposition is true

(2) For every element a of A such that x ∈ I holds (I ⟼ a)_{x} = a.

Let us consider x_{1}, x_{2}, y_{1}, y_{2}. The functor [x_{1} ⟼ y_{1}, x_{2} ⟼ y_{2}] yields a function and is defined as follows: (Def.2) [x_{1} ⟼ y_{1}, x_{2} ⟼ y_{2}] = ({x_{1}} ⟼ y_{1}) +· ({x_{2}} ⟼ y_{2}).

The following propositions are true:

(3) dom[x_{1} ⟼ y_{1}, x_{2} ⟼ y_{2}] = {x_{1}, x_{2}} and rng[x_{1} ⟼ y_{1}, x_{2} ⟼ y_{2}] ⊆ {y_{1}, y_{2}}.

(4) If x_{1} ≠ x_{2}, then [x_{1} ⟼ y_{1}, x_{2} ⟼ y_{2}](x_{1}) = y_{1} and [x_{1} ⟼ y_{1}, x_{2} ⟼ y_{2}](x_{2}) = y_{2}.

(5) If x_{1} ≠ x_{2}, then rng[x_{1} ⟼ y_{1}, x_{2} ⟼ y_{2}] = {y_{1}, y_{2}}.

(6) [x_{1} ⟼ y, x_{2} ⟼ y] = {x_{1}, x_{2}} ⟼ y.

Let us consider A, x_{1}, x_{2}, and let y_{1}, y_{2} be elements of A. Then [x_{1} ⟼ y_{1}, x_{2} ⟼ y_{2}] is a function from {x_{1}, x_{2}} into A.

The following proposition is true

(7) If x_{1} ≠ x_{2}, then for all elements y_{1}, y_{2} of A holds [x_{1} ⟼ y_{1}, x_{2} ⟼ y_{2}]_{x_{1}} = y_{1} and [x_{1} ⟼ y_{1}, x_{2} ⟼ y_{2}]_{x_{2}} = y_{2}.

2. Indexed families of morphisms

We now define two new functors. Let us consider C, I, and let F be a function from I into the morphisms of C. The functor dom_{κ} F (κ) yielding a function from I into the objects of C is defined as follows: (Def.3) for every x such that x ∈ I holds (dom_{κ} F (κ))_{x} = dom(F_{x}). The functor cod_{κ} F (κ) yielding a function from I into the objects of C is defined by: (Def.4) for every x such that x ∈ I holds (cod_{κ} F (κ))_{x} = cod(F_{x}).

We now state four propositions:

(8) dom_{κ}(I ⟼ f)(κ) = I ⟼ dom f.

(9) cod_{κ}(I ⟼ f)(κ) = I ⟼ cod f.

(10) dom_{κ}[x_{1} ⟼ p_{1}, x_{2} ⟼ p_{2}](κ) = [x_{1} ⟼ dom p_{1}, x_{2} ⟼ dom p_{2}].

(11) cod_{κ}[x_{1} ⟼ p_{1}, x_{2} ⟼ p_{2}](κ) = [x_{1} ⟼ cod p_{1}, x_{2} ⟼ cod p_{2}].

Let us consider C, I, and let F be a function from I into the morphisms of C. The functor F^{op} yields a function from I into the morphisms of C^{op} and is defined as follows: (Def.5) for every x such that x ∈ I holds (F^{op})_{x} = (F_{x})^{op}.

Next we state three propositions:

(12) (I ⟼ f)^{op} = I ⟼ f^{op}.

(13) If x_{1} ≠ x_{2}, then [x_{1} ⟼ p_{1}, x_{2} ⟼ p_{2}]^{op} = [x_{1} ⟼ p_{1}^{op}, x_{2} ⟼ p_{2}^{op}].

(14) For every function F from I into the morphisms of C holds (F^{op})^{op} = F. Let us consider C, I, and let F be a function from I into the morphisms of

C^{op}. The functor ^{op}F yielding a function from I into the morphisms of C is defined by: (Def.6) for every x such that x ∈ I holds (^{op}F)_{x} = ^{op}(F_{x}).

The following propositions are true:

(15) For every morphism f of C^{op} holds ^{op}(I ⟼ f) = I ⟼ ^{op}f.

(16) If x_{1} ≠ x_{2}, then for all morphisms p_{1}, p_{2} of C^{op} holds ^{op}[x_{1} ⟼ p_{1}, x_{2} ⟼ p_{2}] = [x_{1} ⟼ ^{op}p_{1}, x_{2} ⟼ ^{op}p_{2}].

(17) For every function F from I into the morphisms of C holds^{op}(F^{op}) = F. We now define two new functors. Let us consider C, I, and let F be a

function from I into the morphisms of C, and let us consider f. The functor F · f yields a function from I into the morphisms of C and is defined as follows: (Def.7) for every x such that x ∈ I holds (F · f)_{x} = F_{x} · f. The functor f · F yielding a function from I into the morphisms of C is defined by: (Def.8) for every x such that x ∈ I holds (f · F)_{x} = f · F_{x}.

The following four propositions are true:

(18) If x_{1} ≠ x_{2}, then [x_{1} ⟼ p_{1}, x_{2} ⟼ p_{2}] · f = [x_{1} ⟼ p_{1} · f, x_{2} ⟼ p_{2} · f].

(19) If x_{1} ≠ x_{2}, then f · [x_{1} ⟼ p_{1}, x_{2} ⟼ p_{2}] = [x_{1} ⟼ f · p_{1}, x_{2} ⟼ f · p_{2}].

(20) For every function F from I into the morphisms of C such that dom_{κ} F (κ) = I ⟼ cod f holds dom_{κ} F · f(κ) = I ⟼ dom f and cod_{κ} F · f(κ) = cod_{κ} F (κ).

(21) For every function F from I into the morphisms of C such that cod_{κ} F (κ) = I ⟼ dom f holds dom_{κ} f · F (κ) = dom_{κ} F (κ) and cod_{κ} f · F (κ) = I ⟼ cod f.

Let us consider C, I, and let F, G be functions from I into the morphisms of C. The functor F · G yields a function from I into the morphisms of C and is defined by: (Def.9) for every x such that x ∈ I holds (F · G)_{x} = F_{x} · G_{x}.

We now state four propositions:

(22) For all functions F, G from I into the morphisms of C such that dom_{κ} F (κ) = cod_{κ} G(κ) holds dom_{κ} F · G(κ) = dom_{κ} G(κ) and cod_{κ} F · G(κ) = cod_{κ} F (κ).

(23) If x_{1} ≠ x_{2}, then [x_{1} ⟼ p_{1}, x_{2} ⟼ p_{2}] · [x_{1} ⟼ q_{1}, x_{2} ⟼ q_{2}] = [x_{1} ⟼ p_{1} · q_{1}, x_{2} ⟼ p_{2} · q_{2}].

(24) For every function F from I into the morphisms of C holds F · f = F · (I ⟼ f).

(25) For every function F from I into the morphisms of C holds f · F = (I ⟼ f) · F.

3. Retractions and coretractions

We now define two new attributes. Let us consider C. A morphism of C is retraction if:

(Def.10) there exists g such that cod g = dom it and it · g = id_{cod it}.

A morphism of C is coretraction if: (Def.11) there exists g such that dom g = cod it and g · it = id_{dom it}.

The following propositions are true:

(26) If f is retraction, then f is epi.

(27) If f is coretraction, then f is monic.

(28) If f is retraction and g is retraction and dom g = cod f, then g · f is retraction.

(29) If f is coretraction and g is coretraction and dom g = cod f, then g · f is coretraction.

(30) If dom g = cod f and g · f is retraction, then g is retraction.

(31) If dom g = cod f and g · f is coretraction, then f is coretraction.

(32) If f is retraction and f is monic, then f is invertible.

(33) If f is coretraction and f is epi, then f is invertible.

(34) f is invertible if and only if f is retraction and f is coretraction.

(35) For every functor T from C to D such that f is retraction holds T (f) is retraction.

(36) For every functor T from C to D such that f is coretraction holds T (f) is coretraction.

(37) f is retraction if and only if f^{op} is coretraction.

(38) f is coretraction if and only if f^{op} is retraction.

4. Morphisms determined by a terminal object

Let us consider C, a, b. Let us assume that b is a terminal object. |_{b}a is a morphism from a to b.

Next we state three propositions:

(39) If b is a terminal object, then dom|_{b}a = a and cod|_{b}a = b.

(40) If b is a terminal object and dom f = a and cod f = b, then |_{b}a = f.

(41) For every morphism f from a to b such that b is a terminal object holds |_{b}a = f.

5. Morphisms determined by an iniatial object

Let us consider C, a, b. Let us assume that a is an initial object. |^{a}b is a morphism from a to b.

Next we state three propositions:

(42) If a is an initial object, then dom|^{a}b = a and cod|^{a}b = b.

(43) If a is an initial object and dom f = a and cod f = b, then |^{a}b = f.

(44) For every morphism f from a to b such that a is an initial object holds |^{a}b = f.

6. Products

Let us consider C, a, I. A function from I into the morphisms of C is said to be a projections family from a onto I if:

(Def.12) dom_{κ} it(κ) = I ⟼ a.

We now state several propositions:

(45) For every projections family F from a onto I such that x ∈ I holds dom(F_{x}) = a.

(46) For every function F from ∅ into the morphisms of C holds F is a projections family from a onto ∅.

(47) If dom f = a, then {y} ⟼ f is a projections family from a onto {y}.

(48) If dom p_{1} = a and dom p_{2} = a, then [x_{1} ⟼ p_{1}, x_{2} ⟼ p_{2}] is a projections family from a onto {x_{1}, x_{2}}.

(49) For every projections family F from a onto ∅ holds F = .

(50) For every projections family F from a onto I such that cod f = a holds F · f is a projections family from dom f onto I.

(51) For every function F from I into the morphisms of C and for every projections family G from a onto I such that dom_{κ} F (κ) = cod_{κ} G(κ) holds F · G is a projections family from a onto I.

(52) For every projections family F from cod f onto I holds f^{op} · F^{op} =

(F · f)^{op}. Let us consider C, a, I, and let F be a function from I into the morphisms

of C. We say that a is a product w.r.t. F if and only if the conditions (Def.13) is satisfied.

(Def.13) (i) F is a projections family from a onto I,

(ii) for every b and for every projections family F′ from b onto I such that cod_{κ} F (κ) = cod_{κ} F′(κ) there exists h such that h ∈ hom(b, a) and for every k such that k ∈ hom(b, a) holds for every x such that x ∈ I holds F_{x} · k = F′_{x} if and only if h = k.

One can prove the following propositions:

(53) For every projections family F from c onto I and for every projections family F′ from d onto I such that c is a product w.r.t. F and d is a product w.r.t. F′ and cod_{κ} F (κ) = cod_{κ} F′(κ) holds c and d are isomorphic.

(54) For every projections family F from c onto I such that c is a product w.r.t. F and for all x_{1}, x_{2} such that x_{1} ∈ I and x_{2} ∈ I holds hom(cod(F_{x_{1}}), cod(F_{x_{2}})) ≠ ∅ and for every x such that x ∈ I holds F_{x} is retraction.

(55) For every function F from ∅ into the morphisms of C holds a is a product w.r.t. F if and only if a is a terminal object.

(56) For every projections family F from a onto I such that a is a product w.r.t. F and dom f = b and cod f = a and f is invertible holds b is a product w.r.t. F · f.

(57) a is a product w.r.t. {y} ⟼ id_{a}.

(58) For every projections family F from a onto I such that a is a product w.r.t. F and for every x such that x ∈ I holds cod(F_{x}) is a terminal object holds a is a terminal object.

Let us consider C, c, p_{1}, p_{2}. We say that c is a product w.r.t. p_{1} and p_{2} if and only if the conditions (Def.14) is satisfied.

(Def.14) (i) dom p_{1} = c, (ii) dom p_{2} = c, (iii) for all d, f, g such that f ∈ hom(d, cod p_{1}) and g ∈ hom(d, cod p_{2}) there

exists h such that h ∈ hom(d, c) and for every k such that k ∈ hom(d, c) holds p_{1} · k = f and p_{2} · k = g if and only if h = k.

The following propositions are true:

(59) If x_{1} ≠ x_{2}, then c is a product w.r.t. p_{1} and p_{2} if and only if c is a product w.r.t. [x_{1} ⟼ p_{1}, x_{2} ⟼ p_{2}].

(60) Suppose hom(c, a) ≠ ∅ and hom(c, b) ≠ ∅. Let p_{1} be a morphism from c to a. Let p_{2} be a morphism from c to b. Then c is a product w.r.t. p_{1} and p_{2} if and only if for every d such that hom(d, a) ≠ ∅ and hom(d, b) ≠ ∅ holds hom(d, c) ≠ ∅ and for every morphism f from d to a and for every morphism g from d to b there exists a morphism h from d to c such that for every morphism k from d to c holds p_{1} · k = f and p_{2} · k = g if and only if h = k.

(61) If c is a product w.r.t. p_{1} and p_{2} and d is a product w.r.t. q_{1} and q_{2} and cod p_{1} = cod q_{1} and cod p_{2} = cod q_{2}, then c and d are isomorphic.

(62) If c is a product w.r.t. p_{1} and p_{2} and hom(cod p_{1}, cod p_{2}) ≠ ∅ and hom(cod p_{2}, cod p_{1}) ≠ ∅, then p_{1} is retraction and p_{2} is retraction.

(63) If c is a product w.r.t. p_{1} and p_{2} and h ∈ hom(c, c) and p_{1} · h = p_{1} and p_{2} · h = p_{2}, then h = id_{c}.

(64) If c is a product w.r.t. p_{1} and p_{2} and dom f = d and cod f = c and f is invertible, then d is a product w.r.t. p_{1} · f and p_{2} · f.

(65) If c is a product w.r.t. p_{1} and p_{2} and cod p_{2} is a terminal object, then c and cod p_{1} are isomorphic.

(66) If c is a product w.r.t. p_{1} and p_{2} and cod p_{1} is a terminal object, then c and cod p_{2} are isomorphic.

7. Coproducts

Let us consider C, c, I. A function from I into the morphisms of C is said to be a injections family into c on I if:

(Def.15) cod_{κ} it(κ) = I ⟼ c.

We now state a number of propositions:

(67) For every injections family F into c on I such that x ∈ I holds cod(F_{x}) = c.

(68) For every function F from ∅ into the morphisms of C holds F is a injections family into a on ∅.

(69) If cod f = a, then {y} ⟼ f is a injections family into a on {y}.

(70) If cod p_{1} = c and cod p_{2} = c, then [x_{1} ⟼ p_{1}, x_{2} ⟼ p_{2}] is a injections family into c on {x_{1}, x_{2}}.

(71) For every injections family F into c on ∅ holds F = .

(72) For every injections family F into b on I such that dom f = b holds f · F is a injections family into cod f on I.

(73) For every injections family F into b on I and for every function G from I into the morphisms of C such that dom_{κ} F (κ) = cod_{κ} G(κ) holds F · G is a injections family into b on I.

(74) For every function F from I into the morphisms of C holds F is a projections family from c onto I if and only if F^{op} is a injections family into c^{op} on I.

(75) For every function F from I into the morphisms of C^{op} and for every object c of C^{op} holds F is a injections family into c on I if and only if opF is a projections family from ^{op}c onto I.

(76) For every injections family F into dom f on I holds F^{op}·f^{op} = (f · F)^{op}. Let us consider C, c, I, and let F be a function from I into the morphisms of

C. We say that c is a coproduct w.r.t. F if and only if the conditions (Def.16) is satisfied.

(Def.16) (i) F is a injections family into c on I,

(ii) for every d and for every injections family F′ into d on I such that dom_{κ} F (κ) = dom_{κ} F′(κ) there exists h such that h ∈ hom(c, d) and for every k such that k ∈ hom(c, d) holds for every x such that x ∈ I holds k · F_{x} = F′_{x} if and only if h = k.

One can prove the following propositions:

(77) For every function F from I into the morphisms of C holds c is a product w.r.t. F if and only if c^{op} is a coproduct w.r.t. F^{op}.

(78) For every injections family F into c on I and for every injections family F′ into d on I such that c is a coproduct w.r.t. F and d is a coproduct w.r.t. F′ and dom_{κ} F (κ) = dom_{κ} F′(κ) holds c and d are isomorphic.

(79) For every injections family F into c on I such that c is a coproduct w.r.t. F and for all x_{1}, x_{2} such that x_{1} ∈ I and x_{2} ∈ I holds hom(dom(F_{x_{1}}), dom(F_{x_{2}})) ≠ ∅ and for every x such that x ∈ I holds F_{x} is coretraction.

(80) For every injections family F into a on I such that a is a coproduct w.r.t. F and dom f = a and cod f = b and f is invertible holds b is a coproduct w.r.t. f · F.

(81) For every injections family F into a on ∅ holds a is a coproduct w.r.t. F if and only if a is an initial object.

(82) a is a coproduct w.r.t. {y} ⟼ id_{a}.

(83) For every injections family F into a on I such that a is a coproduct w.r.t. F and for every x such that x ∈ I holds dom(F_{x}) is an initial object holds a is an initial object.

Let us consider C, c, i_{1}, i_{2}. We say that c is a coproduct w.r.t. i_{1} and i_{2} if and only if the conditions (Def.17) is satisfied.

(Def.17) (i) cod i_{1} = c, (ii) cod i_{2} = c, (iii) for all d, f, g such that f ∈ hom(dom i_{1}, d) and g ∈ hom(dom i_{2}, d)

there exists h such that h ∈ hom(c, d) and for every k such that k ∈ hom(c, d) holds k · i_{1} = f and k · i_{2} = g if and only if h = k.

We now state several propositions:

(84) c is a product w.r.t. p_{1} and p_{2} if and only if c^{op} is a coproduct w.r.t. p_{1}^{op} and p_{2}^{op}.

(85) If x_{1} ≠ x_{2}, then c is a coproduct w.r.t. i_{1} and i_{2} if and only if c is a coproduct w.r.t. [x_{1} ⟼ i_{1}, x_{2} ⟼ i_{2}].

(86) If c is a coproduct w.r.t. i_{1} and i_{2} and d is a coproduct w.r.t. j_{1} and j_{2} and dom i_{1} = dom j_{1} and dom i_{2} = dom j_{2}, then c and d are isomorphic.

(87) Suppose hom(a, c) ≠ ∅ and hom(b, c) ≠ ∅. Let i_{1} be a morphism from a to c. Let i_{2} be a morphism from b to c. Then c is a coproduct w.r.t. i_{1} and i_{2} if and only if for every d such that hom(a, d) ≠ ∅ and hom(b, d) ≠ ∅ holds hom(c, d) ≠ ∅ and for every morphism f from a to d and for every

products and coproducts in categories 709

morphism g from b to d there exists a morphism h from c to d such that for every morphism k from c to d holds k · i_{1} = f and k · i_{2} = g if and only if h = k.

(88) If c is a coproduct w.r.t. i_{1} and i_{2} and hom(dom i_{1}, dom i_{2}) ≠ ∅ and hom(dom i_{2}, dom i_{1}) ≠ ∅, then i_{1} is coretraction and i_{2} is coretraction.

(89) If c is a coproduct w.r.t. i_{1} and i_{2} and h ∈ hom(c, c) and h · i_{1} = i_{1} and h · i_{2} = i_{2}, then h = id_{c}.

(90) If c is a coproduct w.r.t. i_{1} and i_{2} and dom f = c and cod f = d and f is invertible, then d is a coproduct w.r.t. f · i_{1} and f · i_{2}.

(91) If c is a coproduct w.r.t. i_{1} and i_{2} and dom i_{2} is an initial object, then dom i_{1} and c are isomorphic.

(92) If c is a coproduct w.r.t. i_{1} and i_{2} and dom i_{1} is an initial object, then dom i_{2} and c are isomorphic.

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

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

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

[7] Zbigniew Semadeni and Antoni Wiweger. Wstȩp do teorii kategorii i funktorów. Volume 45 of Biblioteka Matematyczna, PWN, Warszawa, 1978.

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

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

710

Transpose Matrices and Groups of Permutations

Katarzyna Jankowska Warsaw University Białystok

Summary. Some facts concerning matrices with dimention 2 × 2 are shown. Upper and lower triangular matrices, and operation of deleting rows and columns in a matrix are introduced. Besides, we deal with sets of permutations and the fact that all permutations of finite set constitute a finite group is proved. Some proofs are based on [11] and [14].

MML Identifier: MATRIX 2.

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

1. Some examples of matrices

For simplicity we follow a convention: x, x_{1}, x_{2}, y_{1}, y_{2} are arbitrary, i, j, k, n, m are natural numbers, D is a non-empty set, K is a field, s is a finite sequence, and a, b, c, d are elements of D. The scheme SeqDEx concerns a non-empty set A, a natural number B, and a binary predicate P, and states that:

there exists a finite sequence p of elements of A such that dom p = Seg B and for every k such that k ∈ Seg B holds P[k, p(k)] provided the following requirement is met:

• for every k such that k ∈ Seg B there exists an element x of A such that P[k, x].

Let us consider D, a, b. Then ⟨a, b⟩ is a finite sequence of elements of D.

Let us consider n, m, and let a be arbitrary. The functor ( \begin{matrix}a & … & a \\ ⋮ & ... & ⋮ \\ a & … & a \end{matrix} )^{n×m}

yielding a tabular finite sequence is defined as follows:

712 katarzyna jankowska

(Def.1) ( \begin{matrix}a & … & a \\ ⋮ & ... & ⋮ \\ a & … & a \end{matrix} )^{n×m} = n ⟼ (m ⟼ a).

Let us consider D, n, m, d. Then ( \begin{matrix}d & … & d \\ ⋮ & ... & ⋮ \\ d & … & d \end{matrix} )^{n×m} is a matrix over D of dimension n × m.

Next we state the proposition

(1) If ⟨⟨i, j⟩⟩ ∈ the indices of ( \begin{matrix}a & … & a \\ ⋮ & ... & ⋮ \\ a & … & a \end{matrix} )^{n×m}, then

(( \begin{matrix}a & … & a \\ ⋮ & ... & ⋮ \\ a & … & a \end{matrix} )^{n×m})_{i,j} = a.

In the sequel a′, b′ are elements of the carrier of K. Next we state the proposition

(2) ( \begin{matrix}a′ & … & a′ \\ ⋮ & ... & ⋮ \\ a′ & … & a′ \end{matrix} )^{n×n}+( \begin{matrix}b′ & … & b′ \\ ⋮ & ... & ⋮ \\ b′ & … & b′ \end{matrix} )^{n×n} = ( \begin{matrix}a′ + b′ & … & a′ + b′ \\ ⋮ & ... & ⋮ \\ a′ + b′ & … & a′ + b′ \end{matrix} )^{n×n}.

Let a, b, c, d be arbitrary. The functor ( \begin{matrix}a & b \\ c & d \end{matrix} ) yielding a tabular finite sequence is defined as follows:

(Def.2) ( \begin{matrix}a & b \\ c & d \end{matrix} ) = ⟨⟨a, b⟩, ⟨c, d⟩⟩.

The following two propositions are true:

(3) len ( \begin{matrix}x_{1} & x_{2} \\ y_{1} & y_{2} \end{matrix} ) = 2 and width ( \begin{matrix}x_{1} & x_{2} \\ y_{1} & y_{2} \end{matrix} ) = 2 and the indices of

( \begin{matrix}x_{1} & x_{2} \\ y_{1} & y_{2} \end{matrix} ) = [: Seg 2, Seg 2 :].

(4) ⟨⟨1, 1⟩⟩ ∈ the indices of ( \begin{matrix}x_{1} & x_{2} \\ y_{1} & y_{2} \end{matrix} ) and ⟨⟨1, 2⟩⟩ ∈ the indices of

( \begin{matrix}x_{1} & x_{2} \\ y_{1} & y_{2} \end{matrix} )

and ⟨⟨2, 1⟩⟩ ∈ the indices of ( \begin{matrix}x_{1} & x_{2} \\ y_{1} & y_{2} \end{matrix} ) and ⟨⟨2, 2⟩⟩ ∈ the indices of

( \begin{matrix}x_{1} & x_{2} \\ y_{1} & y_{2} \end{matrix} ).

Let us consider D, and let a be an element of D. Then ⟨a⟩ is an element of D^{1}.

Let us consider D, and let us consider n, and let p be an element of D^{n}. Then ⟨p⟩ is a matrix over D of dimension 1 × n.

One can prove the following proposition

(5) ⟨⟨1, 1⟩⟩ ∈ the indices of ⟨⟨a⟩⟩ and ⟨⟨a⟩⟩_{1,1} = a.

Let us consider D, and let a, b, c, d be elements of D. Then ( \begin{matrix}a & b \\ c & d \end{matrix} ) is a

matrix over D of dimension 2.

Next we state the proposition

(6) ( \begin{matrix}a & b \\ c & d \end{matrix} )_{1,1} = a and ( \begin{matrix}a & b \\ c & d \end{matrix} )_{1,2} = b and ( \begin{matrix}a & b \\ c & d \end{matrix} )_{2,1} = c and

( \begin{matrix}a & b \\ c & d \end{matrix} )_{2,2} = d.

Let us consider n, and let K be a field. A matrix over K of dimension n is said to be an upper triangular matrix over K of dimension n if: (Def.3) for all i, j such that ⟨⟨i, j⟩⟩ ∈ the indices of it holds if i > j, then

it_{i,j} = 0_{K}. Let us consider n, K. A matrix over K of dimension n is said to be a lower

triangular matrix over K of dimension n if: (Def.4) for all i, j such that ⟨⟨i, j⟩⟩ ∈ the indices of it holds if i < j, then

it_{i,j} = 0_{K}. The following proposition is true

(7) For every matrix M over D such that len M = n holds M is a matrix over D of dimension n × width M.

2. Deleting of rows and columns in a matrix

Let us consider i, and let p be a finite sequence. Let us assume that i ∈ dom p. The functor p_{i} yielding a finite sequence is defined by: (Def.5) p_{i} = p · Sgm(Seg len p \ {i}).

We now state three propositions:

(8) For every finite sequence p such that len p > 0 and for every i such that i ∈ dom p there exists m such that len p = m + 1 and len(p_{i}) = m.

(9) For every finite sequence p of elements of D and for every i such that i ∈ dom p holds p_{i} is a finite sequence of elements of D.

(10) For every matrix M over K of dimension n × m and for every k such

that k ∈ Seg n holds M(k) = Line(M, k). Let us consider i, and let us consider K, and let M be a matrix over K.

Let us assume that i ∈ Seg width M. The deleting of i-column in M yielding a matrix over K is defined as follows: (Def.6) len(the deleting of i-column in M) = len M and for every k such that

k ∈ Seg len M holds (the deleting of i-column in M)(k) = Line(M, k)_{i}.

The following propositions are true:

(11) For all matrices M_{1}, M_{2} over D holds M_{1} = M_{2} if and only if M_{1}^{T} = M_{2}^{T} and len M_{1} = len M_{2}.

(12) For every matrix M over D such that width M > 0 holds len(M^{T}) = width M and width(M^{T}) = len M.

(13) For all matrices M_{1}, M_{2} over D such that width M_{1} > 0 and width M_{2} > 0 holds M_{1} = M_{2} if and only if M_{1}^{T} = M_{2}^{T} and width(M_{1}^{T}) = width(M_{2}^{T}).

(14) For all matrices M_{1}, M_{2} over D such that width M_{1} > 0 and width M_{2} > 0 holds M_{1} = M_{2} if and only if M_{1}^{T} = M_{2}^{T} and width M_{1} = width M_{2}.

(15) For every matrix M over D such that len M > 0 and width M > 0 holds (M^{T})^{T} = M.

(16) For every matrix M over D and for every i such that i ∈ Seg len M holds Line(M, i) = (M^{T})_{,i} .

(17) For every matrix M over D and for every j such that j ∈ Seg width M holds Line(M^{T}, j) = M_{,j} .

(18) For every matrix M over D and for every i such that i ∈ Seg len M

holds M(i) = Line(M, i). Let us consider i, and let us consider K, and let M be a matrix over K. Let

us assume that i ∈ Seg len M and width M > 0. The deleting of i-row in M yields a matrix over K and is defined by: (Def.7) (i) the deleting of i-row in M = ε if len M = 1,

(ii) width(the deleting of i-row in M) = width M and for every k such that k ∈ Seg width M holds (the deleting of i-row in M)_{,k} = (M_{,k} )_{i}, otherwise.

Let us consider i, j, and let us consider n, and let us consider K, and let M be a matrix over K of dimension n. The deleting of i-row and j-column in M yields a matrix over K and is defined as follows: (Def.8) (i) the deleting of i-row and j-column in M = ε if n = 1,

(ii) the deleting of i-row and j-column in M = the deleting of j-column in the deleting of i-row in M, otherwise.

3. Sets of permutations

Let us consider n, and let q, p be permutations of Seg n. Then p · q is a permutation of Seg n.

A set is permutational if: (Def.9) there exists n such that for every x such that x ∈ it holds x is a per-

mutation of Seg n.

Let P be a permutational non-empty set. The functor len P yielding a natural number is defined as follows:

(Def.10) there exists s such that s ∈ P and len P = len s.

Let P be a permutational non-empty set. We see that the element of P is a permutation of Seg len P.

One can prove the following proposition

(19) For every n there exists a permutational non-empty set P such that

len P = n. Let us consider n. The permutations of n-element set constitute a permuta-

tional non-empty set defined as follows: (Def.11) x ∈ the permutations of n-element set if and only if x is a permutation

of Seg n.

The following propositions are true:

(20) len(the permutations of n-element set) = n.

(21) The permutations of 1-element set = {id_{1}}.

Let us consider n, and let p be an element of the permutations of n-element set. The functor len p yields a natural number and is defined as follows:

(Def.12) there exists a finite sequence s such that s = p and len p = len s.

We now state the proposition

(22) For every element p of the permutations of n-element set holds len p = n.

4. Group of permutations

In the sequel p, q denote elements of the permutations of n-element set. Let us consider n. The functor A_{n} yielding a strict half group structure is defined by:

(Def.13) the carrier of A_{n} = the permutations of n-element set and for all elements q, p of the permutations of n-element set holds (the operation of A_{n})(q, p) = p · q.

One can prove the following propositions:

(23) id_{n} is an element of A_{n}.

(24) p · id_{n} = p and id_{n} · p = p.

(25) p · p^{−1} = id_{n} and p^{−1} · p = id_{n}.

(26) p^{−1} is an element of A_{n}.

(27) p is an element of A_{n} if and only if p is an element of the permutations

of n-element set. Let us consider n. A permutation of n element set is an element of the

permutations of n-element set.

Then A_{n} is a strict group. We now state the proposition

(28) id_{n} = 1_{A_{n}}.

Let us consider n, and let p be a permutation of Seg n. We say that p is a transposition if and only if:

716 katarzyna jankowska

(Def.14) there exist i, j such that i ∈ dom p and j ∈ dom p and i ≠ j and p(i) = j and p(j) = i and for every k such that k ≠ i and k ≠ j and k ∈ dom p holds p(k) = k.

We now define two new predicates. Let us consider n, and let p be a permutation of Seg n. We say that p is even if and only if:

(Def.15) there exists a finite sequence l of elements of the carrier of A_{n} such that len l mod 2 = 0 and p = ∏ l and for every i such that i ∈ dom l there exists q such that l(i) = q and q is a transposition.

p is odd stands for p is not even.

We now state the proposition

(29) id_{Seg n} is even.

Let us consider K, n, and let x be an element of the carrier of K, and let p be an element of the permutations of n-element set. The functor (−1)^{sgn(p)}x yields an element of the carrier of K and is defined by:

(Def.16) (i) (−1)^{sgn(p)}x = x if p is even, (ii) (−1)^{sgn(p)}x = −x, otherwise.

Let X be a set. Let us assume that X is finite. The functor Ω_{X}^{f} yields an element of Fin X and is defined as follows:

(Def.17) Ω_{X}^{f} = X.

We now state the proposition

(30) The permutations of n-element set is finite.

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. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[5] Czesław Byliński. Binary operations applied to finite sequences. Formalized Mathematics, 1(4):643–649, 1990.

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

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

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

[9] Czesław Byliński. Semigroup operations on finite subsets. Formalized Mathematics, 1(4):651–656, 1990.

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

[11] Thomas W. Hungerford. Algebra. Volume 73 of Graduate Texts in Mathematics, Springer-Verlag New York Inc., Seattle, Washington USA, Department of Mathematics University of Washington edition, 1974.

[12] Katarzyna Jankowska. Matrices. Abelian group of matrices. Formalized Mathematics, 2(4):475–480, 1991.

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

transpose matrices and groups of permutations 717

[14] Serge Lang. Algebra. PWN, Warszawa, 1984.

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

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

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

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

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

[20] Wojciech A. Trybulec. Lattice of subgroups of a group. Frattini subgroup. Formalized Mathematics, 2(1):41–47, 1991.

[21] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569–573, 1990.

718

Complete Lattices

Grzegorz Bancerek Warsaw University, Białystok Polish Academy of Sciences, Warsaw

Summary. In the first section the lattice of subsets of distinct set is introduced. The join and meet operations are, respectively, union and intersection of sets, and the ordering relation is inclusion. It is shown that this lattice is Boolean, i.e. distributive and complimentary. The socond section introduced the poset generated in a distinct lattice by its ordering relation. Besides, it is proved that posets which have l.u.b.’s and g.l.b.’s for every two elements generate lattices with the same ordering relations. In the last section the concept of complete lattice is introduced and discussed. Finally, the fact that the function f from subsets of distinct set yielding elements of this set is a infinite union of some complete lattice, if f yields an element a for singleton {a} and f(f^{∘}X) = f(⨆ X) for every subset X, is proved. Some concepts and proofs are based on [6] and [7].

MML Identifier: LATTICE3.

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

1. Boolean lattice of subsets

Let X be a non-empty set, and let x, y be elements of X. Then {x, y} is a non-empty subset of X.

Let X be a set, and let x, y be elements of 2^{X}. Then x ∪ y is a subset of X. Then x ∩ y is a subset of X.

Let X be a set. The lattice of subsets of X yields a strict lattice structure and is defined by: (Def.1) the carrier of the lattice of subsets of X = 2^{X} and for all elements

Y, Z of 2^{X} holds (the join operation of the lattice of subsets of X)(Y, Z) = Y ∪ Z and (the meet operation of the lattice of subsets of X)(Y, Z) = Y ∩ Z.

In the sequel X will denote a set and x, y will denote elements of the lattice of subsets of X. The following propositions are true:

(1) x ⊔ y = x ∪ y and x ⊓ y = x ∩ y.

(2) x ⊑ y if and only if x ⊆ y. Let us consider X. Then the lattice of subsets of X is a strict lattice. In the sequel x will denote an element of the lattice of subsets of X. The

following propositions are true:

(3) The lattice of subsets of X is a lower bound lattice and ⊥_{the lattice of subsets of X} = ∅.

(4) The lattice of subsets of X is an upper bound lattice and ⊤_{the lattice of subsets of X} = X.

Let us consider X. Then the lattice of subsets of X is a strict Boolean lattice. Next we state the proposition

(5) For every element x of the lattice of subsets of X holds x^{c} = X \ x.

2. Correspondence between lattices and posets

Let L be a lattice. Then LattRel(L) is an order in the carrier of L.

Let L be a lattice. The functor Poset(L) yields a strict poset and is defined as follows: (Def.2) Poset(L) = ⟨the carrier of L, LattRel(L)⟩.

Next we state the proposition

(6) For all lattices L_{1}, L_{2} such that Poset(L_{1}) = Poset(L_{2}) holds the lattice structure of L_{1} = the lattice structure of L_{2}.

Let L be a lattice, and let p be an element of L. The functor p^{·} yields an element of Poset(L) and is defined as follows: (Def.3) p^{·} = p.

Let L be a lattice, and let p be an element of Poset(L). The functor ^{·}p yielding an element of L is defined as follows: (Def.4) ^{·}p = p.

In the sequel L is a lattice, p, q are elements of L, and p′ is an element of Poset(L). We now state the proposition

(7) p ⊑ q if and only if p^{·} ≤ q^{·}. Let X be a set, and let O be an order in X. Then O^{}is an order in X. Let A be a poset. The functor A^{}yields a strict poset and is defined as

follows: (Def.5) A^{}= ⟨the carrier of A, (the order of A)^{}⟩.

In the sequel A will be a poset and a, b, c will be elements of A. One can prove the following proposition

(8) (A^{})^{}= the poset of A.

Let A be a poset, and let a be an element of A. The functor a^{}yielding an element of A^{}is defined as follows: (Def.6) a^{}= a.

Let A be a poset, and let a be an element of A^{}. The functor a yielding an element of A is defined by: (Def.7) a = a.

One can prove the following proposition

(9) a ≤ b if and only if b^{}≤ a^{}. We now define four new predicates. Let A be a poset, and let X be a set,

and let a be an element of A. The predicate a ≤ X is defined as follows: (Def.8) for every element b of A such that b ∈ X holds a ≤ b. We write X ≥ a if a ≤ X. The predicate X ≤ a is defined by: (Def.9) for every element b of A such that b ∈ X holds b ≤ a. We write a ≥ X if and only if X ≤ a.

We now define two new attributes. A poset has l.u.b.’s if: (Def.10) for every elements x, y of it there exists an element z of it such that

x ≤ z and y ≤ z and for every element z′ of it such that x ≤ z′ and y ≤ z′ holds z ≤ z′.

A poset has g.l.b.’s if: (Def.11) for every elements x, y of it there exists an element z of it such that

z ≤ x and z ≤ y and for every element z′ of it such that z′ ≤ x and z′ ≤ y holds z′ ≤ z.

We now state two propositions:

(10) A has l.u.b.’s if and only if A^{}has g.l.b.’s.

(11) For every lattice L holds Poset(L) has l.u.b.’s and g.l.b.’s.

A poset is complete if: (Def.12) for every set X there exists an element a of it such that X ≤ a and for

every element b of it such that X ≤ b holds a ≤ b.

Next we state the proposition

(12) If A is complete, then A has l.u.b.’s and g.l.b.’s.

Let A be a poset satisfying the condition: A has l.u.b.’s. Let a, b be elements of A. The functor a ⊔ b yielding an element of A is defined as follows:

(Def.13) a ≤ a ⊔ b and b ≤ a ⊔ b and for every element c of A such that a ≤ c and b ≤ c holds a ⊔ b ≤ c.

Let A be a poset satisfying the condition: A has g.l.b.’s. Let a, b be elements of A. The functor a ⊓ b yields an element of A and is defined as follows:

(Def.14) a ⊓ b ≤ a and a ⊓ b ≤ b and for every element c of A such that c ≤ a and c ≤ b holds c ≤ a ⊓ b.

For simplicity we follow a convention: V denotes a poset with l.u.b.’s, u_{1}, u_{2}, u_{3} denote elements of V, N denotes a poset with g.l.b.’s, n_{1}, n_{2}, n_{3} denote elements of N, K denotes a poset with l.u.b.’s and g.l.b.’s, and k_{1}, k_{2} denote elements of K. The following propositions are true:

(13) u_{1} ⊔ u_{2} = u_{2} ⊔ u_{1}.

(14) (u_{1} ⊔ u_{2}) ⊔ u_{3} = u_{1} ⊔ (u_{2} ⊔ u_{3}).

(15) n_{1} ⊓ n_{2} = n_{2} ⊓ n_{1}.

(16) (n_{1} ⊓ n_{2}) ⊓ n_{3} = n_{1} ⊓ (n_{2} ⊓ n_{3}).

(17) k_{1} ⊓ k_{2} ⊔ k_{2} = k_{2}.

(18) k_{1} ⊓ (k_{1} ⊔ k_{2}) = k_{1}.

(19) For every A being a poset with l.u.b.’s and g.l.b.’s there exists a strict

lattice L such that the poset of A = Poset(L). Let us consider A satisfying the condition: A has l.u.b.’s and g.l.b.’s. The

functor _{A} yields a strict lattice and is defined as follows: (Def.15) the poset of A = Poset( _{A}).

The following proposition is true

(20) LattRel(L)^{}= LattRel(L^{∘}) and Poset(L)^{}= Poset(L^{∘}).

3. Complete lattices

Let L be a lattice structure. A subset of L is a subset of the carrier of L.

We now define four new predicates. Let L be a lattice structure, and let p be an element of L, and let X be a set. The predicate p ⊑ X is defined by:

(Def.16) for every element q of L such that q ∈ X holds p ⊑ q.

We write X ⊒ p if p ⊑ X. The predicate X ⊑ p is defined by: (Def.17) for every element q of L such that q ∈ X holds q ⊑ p.

We write p ⊒ X if X ⊑ p.

We now state two propositions:

(21) For every lattice L and for all elements p, q, r of L holds p ⊑ {q, r} if and only if p ⊑ q ⊓ r.

(22) For every lattice L and for all elements p, q, r of L holds p ⊒ {q, r} if

and only if q ⊔ r ⊑ p. We now define three new attributes. A lattice structure is complete if:

(Def.18) for every set X there exists an element p of it such that X ⊑ p and for

every element r of it such that X ⊑ r holds p ⊑ r. A lattice structure is ⨆-distributive if it satisfies the condition (Def.19).

(Def.19) Given X. Let a, b, c be elements of it. Then if X ⊑ a and for every element d of it such that X ⊑ d holds a ⊑ d and {b ⊓ a′ : a′ ∈ X} ⊑ c, where a′ ranges over elements of it and for every element d of it such that {b ⊓ a′ : a′ ∈ X} ⊑ d, where a′ ranges over elements of it holds c ⊑ d, then b ⊓ a ⊑ c.

A lattice structure is ⌈−⌉-distributive if it satisfies the condition (Def.20). (Def.20) Given X. Let a, b, c be elements of it. Then if X ⊒ a and for every

element d of it such that X ⊒ d holds d ⊑ a and {b ⊔ a′ : a′ ∈ X} ⊒ c, where a′ ranges over elements of it and for every element d of it such that {b ⊔ a′ : a′ ∈ X} ⊒ d, where a′ ranges over elements of it holds d ⊑ c, then c ⊑ b ⊔ a.

We now state several propositions:

(23) For every Boolean lattice B and for every element a of B holds X ⊑ a if and only if {b^{c} : b ∈ X} ⊒ a^{c}, where b ranges over elements of B.

(24) For every Boolean lattice B and for every element a of B holds X ⊒ a if and only if {b^{c} : b ∈ X} ⊑ a^{c}, where b ranges over elements of B.

(25) The lattice of subsets of X is complete.

(26) The lattice of subsets of X is ⨆-distributive.

(27) The lattice of subsets of X is ⌈−⌉-distributive.

Next we state four propositions:

(28) p ⊑ X if and only if p^{·} ≤ X.

(29) p′ ≤ X if and only if ^{·}p′ ⊑ X.

(30) X ⊑ p if and only if X ≤ p^{·}.

(31) X ≤ p′ if and only if X ⊑ ^{·}p′.

Let A be a complete poset. Then _{A} is a complete strict lattice.

Let L be a lattice structure satisfying the condition: L is a complete lattice. Let X be a set. The functor ⨆_{L} X yields an element of L and is defined by:

(Def.21) X ⊑ ⨆_{L} X and for every element r of L such that X ⊑ r holds ⨆_{L} X ⊑

r. Let L be a lattice structure, and let X be a set. The functor ⌈−⌉_{L}X yielding

an element of L is defined as follows: (Def.22) ⌈−⌉_{L}X = ⨆_{L}{p : p ⊑ X}, where p ranges over elements of L.

We now define two new functors. Let L be a lattice structure, and let X be a subset of L. We introduce the functor ⨆ X as a synonym of ⨆_{L} X. We introduce the functor ⌈−⌉X as a synonym of ⌈−⌉_{L}X.

We adopt the following rules: C denotes a complete lattice, a, b, c denote elements of C, and X, Y denote sets. Next we state a number of propositions:

(32) ⨆_{C}{a ⊓ b : b ∈ X} ⊑ a ⊓ ⨆_{C} X.

(33) C is ⨆-distributive if and only if for all X, a holds a⊓⨆_{C} X ⊑ ⨆_{C}{a⊓b : b ∈ X}.

(34) a = ⌈−⌉_{C}X if and only if a ⊑ X and for every b such that b ⊑ X holds b ⊑ a.

(35) a ⊔ ⌈−⌉_{C}X ⊑ ⌈−⌉_{C}{a ⊔ b : b ∈ X}.

(36) C is ⌈−⌉-distributive if and only if for all X, a holds ⌈−⌉_{C}{a⊔b : b ∈ X} ⊑ a ⊔ ⌈−⌉_{C}X.

(37) ⨆_{C} X = ⌈−⌉_{C}{a : a ⊒ X}.

(38) If a ∈ X, then a ⊑ ⨆_{C} X and ⌈−⌉_{C}X ⊑ a.

(39) If X ⊑ a, then ⨆_{C} X ⊑ a.

(40) If a ⊑ X, then a ⊑ ⌈−⌉_{C}X.

(41) If a ∈ X and X ⊑ a, then ⨆_{C} X = a.

(42) If a ∈ X and a ⊑ X, then ⌈−⌉_{C}X = a.

(43) ⨆{a} = a and ⌈−⌉{a} = a.

(44) a ⊔ b = ⨆{a, b} and a ⊓ b = ⌈−⌉{a, b}.

(45) a = ⨆_{C}{b : b ⊑ a} and a = ⌈−⌉_{C}{c : a ⊑ c}.

(46) If X ⊆ Y, then ⨆_{C} X ⊑ ⨆_{C} Y and ⌈−⌉_{C}Y ⊑ ⌈−⌉_{C}X.

(47) ⨆_{C} X = ⨆_{C}{a : ⋁_{b}[a ⊑ b ∧ b ∈ X]} and ⌈−⌉_{C}X = ⌈−⌉_{C}{b : ⋁_{a}[a ⊑ b ∧ a ∈ X]}.

(48) If for every a such that a ∈ X there exists b such that a ⊑ b and b ∈ Y, then ⨆_{C} X ⊑ ⨆_{C} Y.

(49) If X ⊆ 2^{the carrier of C}, then ⨆_{C} ⋃ X = ⨆_{C}{⨆ Y : Y ∈ X}, where Y ranges over subsets of C.

(50) C is a lower bound lattice and ⊥_{C} = ⨆_{C} ∅.

(51) C is an upper bound lattice and ⊤_{C} = ⨆_{C} (the carrier of C).

(52) If C is an implicative lattice, then a ⇒ b = ⨆_{C}{c : a ⊓ c ⊑ b}.

(53) If C is an implicative lattice, then C is ⨆-distributive.

(54) For every complete ⨆-distributive lattice D and for every element a of D holds a ⊓ ⨆_{D} X = ⨆_{D}{a ⊓ b_{1} : b_{1} ∈ X}, where b_{1} ranges over elements of D and ⨆_{D} X ⊓ a = ⨆_{D}{b_{2} ⊓ a : b_{2} ∈ X}, where b_{2} ranges over elements of D.

(55) For every complete ⌈−⌉-distributive lattice D and for every element a of D holds a ⊔ ⌈−⌉_{D}X = ⌈−⌉_{D}{a ⊔ b_{1} : b_{1} ∈ X}, where b_{1} ranges over elements of D and ⌈−⌉_{D}X ⊔ a = ⌈−⌉_{D}{b_{2} ⊔ a : b_{2} ∈ X}, where b_{2} ranges over elements of D.

In this article we present several logical schemes. The scheme SingleFraenkel deals with a constant A, a non-empty set B, and a unary predicate P, and states that:

{A : P[a]} = {A}, where a ranges over elements of B provided the parameters meet the following requirement:

• there exists an element a of B such that P[a].

The scheme FuncFraenkel deals with a non-empty set A, a non-empty set B, a unary functor F yielding an element of B, a function C, and a unary predicate P, and states that:

C ^{∘} {F(x) : P[x]} = {C(F(x)) : P[x]}, where x ranges over elements of A, and x ranges over elements of A provided the parameters satisfy the following condition:

• B ⊆ dom C.

The following proposition is true

complete lattices 725

(56) Let D be a non-empty set. Let f be a function from 2^{D} into D. Then if for every element a of D holds f({a}) = a and for every subset X of 2^{D} holds f(f^{∘}X) = f(⋃ X), then there exists a complete strict lattice L such that the carrier of L = D and for every subset X of L holds ⨆ X = f(X).

References

[1] Grzegorz Bancerek. Filters - part I. Formalized Mathematics, 1(5):813–819, 1990.

[2] Grzegorz Bancerek. Filters - part II. Quotient lattices modulo filters and direct product of two lattices. Formalized Mathematics, 2(3):433–438, 1991.

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

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

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

[6] Helena Rasiowa and Roman Sikorski. The Mathematics of Metamathematics. Volume 41 of Monografie Matematyczne, PWN, Warszawa, 1968.

[7] Tadeusz Traczyk. Wstȩp do teorii algebr Boole’a. Volume 37 of Biblioteka Matematyczna, PWN, Warszawa, 1970.

[8] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

[9] Andrzej Trybulec. Finite join and finite meet and dual lattices. Formalized Mathematics, 1(5):983–988, 1990.

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

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

[12] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski - Zorn lemma. Formalized Mathematics, 1(2):387–393, 1990.

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

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

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

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

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

Index of MML Identifiers

BHSP 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 695 CAT 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .701 COMMACAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 679 CQC SIM1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 635 FDIFF 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 653 GR CY 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 623 ISOCAT 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 629 LANG1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 683 LATTICE3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 719 L'HOSPIT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 675 MATRIX 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 711 MEASURE3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 689 METRIC 6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 657 MODCAT 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 649 RINGCAT1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 643 TOPREAL1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 617 TOPREAL2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 663 TSEP 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 665

Contents Form. Math. 2 (5)

Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 615 The Topological Space E_{T}^{2}. Arcs, Line Segments and Special Polygonal Arcs

By Agata Darmochwał and Yatsuka Nakamura . . . . . . . . 617

Cyclic Groups and Some of Their Properties - Part I

By Dariusz Surowik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 623

Isomorphisms of Categories

By Andrzej Trybulec . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 629

Similarity of Formulae

By Agata Darmochwał and Andrzej Trybulec . . . . . . . . . 635

Category of Rings

By Michał Muzalewski . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 643

Category of Left Modules

By Michał Muzalewski . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 649

Real Function One-Side Differantiability

By Ewa Burakowska and Beata Madras . . . . . . . . . . . . . . . . . 653

Sequences in Metric Spaces

By Stanisława Kanas and Adam Lecko . . . . . . . . . . . . . . . . . . . 657

The Topological Space E_{T}^{2}. Simple Closed Curves

By Agata Darmochwał and Yatsuka Nakamura . . . . . . . . 663

Separated and Weakly Separated Subspaces of Topological Spaces

By Zbigniew Karno . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 665

The de l’Hospital Theorem

By Małgorzata Korolkiewicz . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 675

Continued on inside back cover

Comma Category

By Grzegorz Bancerek and Agata Darmochwał . . . . . . . . 679

Context-Free Grammar - Part 1

By Patricia L. Carlson and Grzegorz Bancerek . . . . . . . 683

Completeness of the σ-Additive Measure. Measure Theory

By Józef Białas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 689

Series in Banach and Hilbert Spaces

By Elżbieta Kraszewska and Jan Popiołek . . . . . . . . . . . . . . 695

Products and Coproducts in Categories

By Czesław Byliński . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 701

Transpose Matrices and Groups of Permutations

By Katarzyna Jankowska . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 711

Complete Lattices

By Grzegorz Bancerek . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 719

Index of MML Identifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 726