FORMALIZED MATHEMATICS Volume 13, Number 3, Pages 361–365 University of Białystok, 2005

Properties of First and Second Order Cutting of Binary Relations

Krzysztof Retel School of Mathematical and Computer Sciences Heriot-Watt University Riccarton, Edinburgh EH14 4AS, Scotland

Summary. This paper introduces some notions concerning binary relations according to [9]. It is also an attempt to complement the knowledge contained in the Mizar Mathematical Library regarding binary relations. We define here an image and inverse image of element of set A under binary relation of two sets A, B as image and inverse image of singleton of the element under this relation, respectively. Next, we define “The First Order Cutting Relation of two sets A, B under a subset of the set A” as the union of images of elements of this subset under the relation. We also define “The Second Order Cutting Subset of the Cartesian Product of two sets A, B under a subset of the set A” as an intersection of images of elements of this subset under the subset of the Cartesian Product. The paper also defines first and second projection of binary relations. The main goal of the article is to prove properties and collocations of definitions introduced in this paper.

MML identifier: RELSET 2, version: 7.5.01 4.39.921

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

1. Preliminaries

We adopt the following rules: x, y, X, Y, A, B, C, M are sets and P, Q, R, R_{1}, R_{2} are binary relations.

Let X be a set. We introduce {{∗} : ∗ ∈ X} as a synonym of SmallestPartition (X).

The following propositions are true:

(1) y ∈ {{∗} : ∗ ∈ X} iff there exists x such that y = {x} and x ∈ X.

(2) X = ∅ iff {{∗} : ∗ ∈ X} = ∅.

(3) {{∗} : ∗ ∈ X ∪ Y } = {{∗} : ∗ ∈ X} ∪ {{∗} : ∗ ∈ Y }.

(4) {{∗} : ∗ ∈ X ∩ Y } = {{∗} : ∗ ∈ X} ∩ {{∗} : ∗ ∈ Y }.

(5) {{∗} : ∗ ∈ X \ Y } = {{∗} : ∗ ∈ X} \ {{∗} : ∗ ∈ Y }.

(6) X ⊆ Y iff {{∗} : ∗ ∈ X} ⊆ {{∗} : ∗ ∈ Y }. Let M be a set and let X, Y be families of subsets of M. Then X ∩ Y is a

family of subsets of M.

We now state two propositions:

(7) For all families B_{1}, B_{2} of subsets of M holds Intersect(B_{1}) ∩ Intersect(B_{2}) ⊆ Intersect(B_{1} ∩ B_{2}).

(8) (P ∩ Q) · R ⊆ (P · R) ∩ (Q · R).

2. The First Order Cutting of Binary Relation of Two Sets A, B under Subset of the Set A

Let X, Y be sets, let R be a relation between X and Y, and let x be an element of X. The functor R^{∘}x yielding a subset of Y is defined as follows:

(Def. 1) R^{∘}x = R^{∘}{x}.

The following propositions are true:

(9) y ∈ R^{∘}{x} iff ⟨⟨x, y⟩⟩ ∈ R.

(10) (R_{1} ∪ R_{2})^{∘}{x} = R_{1}^{∘}{x} ∪ R_{2}^{∘}{x}.

(11) (R_{1} ∩ R_{2})^{∘}{x} = R_{1}^{∘}{x} ∩ R_{2}^{∘}{x}.

(12) (R_{1} \ R_{2})^{∘}{x} = R_{1}^{∘}{x} \ R_{2}^{∘}{x}.

(13) (R_{1} ∩ R_{2})^{∘}{{∗} : ∗ ∈ X} ⊆ R_{1}^{∘}{{∗} : ∗ ∈ X} ∩ R_{2}^{∘}{{∗} : ∗ ∈ X}. Let X, Y be sets, let R be a relation between X and Y, and let x be an

element of X. The functor R^{−1}(x) yields a subset of X and is defined by: (Def. 2) R^{−1}(x) = R^{−1}({x}).

One can prove the following propositions:

(14) Let A be a set, F be a family of subsets of A, and R be a binary relation. Then R^{∘} ⋃ F = ⋃{R^{∘}X; X ranges over subsets of A: X ∈ F }.

(15) For every non empty set A and for every subset X of A holds X = ⋃{{x}; x ranges over elements of A: x ∈ X}.

(16) For every non empty set A and for every subset X of A holds {{x}; x ranges over elements of A: x ∈ X} is a family of subsets of A.

(17) Let A be a non empty set, B be a set, X be a subset of A, and R be a relation between A and B. Then R^{∘}X = ⋃{R^{∘}x; x ranges over elements of A: x ∈ X}.

(18) Let A be a non empty set, B be a set, X be a subset of A, and R be a relation between A and B. Then {R^{∘}x; x ranges over elements of A: x ∈ X} is a family of subsets of B.

Let A, B be sets, let R be a subset of [: A, 2^{B}:], and let X be a set. Then R^{∘}X is a family of subsets of B.

Let A be a set and let R be a binary relation. The functor R^{A} yields a function and is defined as follows:

(Def. 3) dom(R^{A}) = 2^{A} and for every set X such that X ⊆ A holds R^{A}(X) =

R^{∘}X. Let B, A be sets and let R be a subset of [: A, B:]. We introduce ^{∘}R as a

synonym of R^{A}.

One can prove the following propositions:

(19) For all sets A, B and for every subset R of [: A, B:] such that X ∈ dom^{∘}R holds (^{∘}R)(X) = R^{∘}X.

(20) For all sets A, B and for every subset R of [: A, B:] holds rng^{∘}R ⊆ 2^{rng R}.

(21) For all sets A, B and for every subset R of [: A, B:] holds ^{∘}R is a function

from 2^{A} into 2^{rng R}. Let B, A be sets and let R be a subset of [: A, B:]. Then ^{∘}R is a function

from 2^{A} into 2^{B}.

Next we state the proposition

(22) For all sets A, B and for every subset R of [: A, B:] holds ⋃((^{∘}R)^{∘}A) ⊆ R^{∘} ⋃ A.

3. The Second Order Cutting of Binary Relation of Two Sets A, B under Subset of the Set A

For simplicity, we adopt the following rules: X, X_{1}, X_{2} are subsets of A, Y is a subset of B, R, R_{1}, R_{2} are subsets of [: A, B:], F is a family of subsets of A, and F_{1} is a family of subsets of [: A, B:].

Let A, B be sets, let X be a subset of A, and let R be a subset of [: A, B:]. The functor R[X] is defined as follows:

(Def. 4) R[X] = Intersect((^{∘}R)^{∘}{{∗} : ∗ ∈ X}).

Let A, B be sets, let X be a subset of A, and let R be a subset of [: A, B:]. Then R[X] is a subset of B.

We now state a number of propositions:

(23) (^{∘}R)^{∘}{{∗} : ∗ ∈ X} = ∅ iff X = ∅.

(24) If y ∈ R[X], then for every set x such that x ∈ X holds y ∈ R^{∘}{x}.

(25) Let B be a non empty set, A be a set, X be a subset of A, y be an element of B, and R be a subset of [: A, B:]. Then y ∈ R[X] if and only if for every set x such that x ∈ X holds y ∈ R^{∘}{x}.

(26) If (^{∘}R)^{∘}{{∗} : ∗ ∈ X_{1}} = ∅, then R[X_{1} ∪ X_{2}] = R[X_{2}].

(27) R[X_{1} ∪ X_{2}] = R[X_{1}] ∩ R[X_{2}].

(28) Let A be a non empty set, B be a set, F be a family of subsets of A, and R be a relation between A and B. Then {R[X]; X ranges over subsets of A: X ∈ F } is a family of subsets of B.

(29) If X = ∅, then R[X] = B.

(30) ⋃ F = ∅ iff for every set X such that X ∈ F holds X = ∅.

(31) Let A be a set, B be a non empty set, R be a relation between A and B, F be a family of subsets of A, and G be a family of subsets of B. If G = {R[Y]; Y ranges over subsets of A: Y ∈ F }, then R[⋃ F] = Intersect(G).

(32) If X_{1} ⊆ X_{2}, then R[X_{2}] ⊆ R[X_{1}].

(33) R[X_{1}] ∪ R[X_{2}] ⊆ R[X_{1} ∩ X_{2}].

(34) (R_{1} ∩ R_{2})[X] = R_{1}[X] ∩ R_{2}[X].

(35) (⋃ F_{1})^{∘}X = ⋃{R^{∘}X; R ranges over subsets of [: A, B:]: R ∈ F_{1}}.

(36) Let F_{1} be a family of subsets of [: A, B:], A, B be sets, and X be a subset of A. Then {R[X]; R ranges over subsets of [: A, B:]: R ∈ F_{1}} is a family of subsets of B.

(37) If R = ∅ and X ≠ ∅, then R[X] = ∅.

(38) If R = [: A, B:], then R[X] = B.

(39) For every family G of subsets of B such that G = {R[X]; R ranges over subsets of [: A, B:]: R ∈ F_{1}} holds (Intersect(F_{1}))[X] = Intersect(G).

(40) If R_{1} ⊆ R_{2}, then R_{1}[X] ⊆ R_{2}[X].

(41) R_{1}[X] ∪ R_{2}[X] ⊆ (R_{1} ∪ R_{2})[X].

(42) y ∈ (R^{c})^{∘}{x} iff ⟨⟨x, y⟩⟩ ∉ R and x ∈ A and y ∈ B.

(43) If X ≠ ∅, then R[X] ⊆ R^{∘}X.

(44) For all sets X, Y holds X meets (R^{⌣})^{∘}Y iff there exist sets x, y such that x ∈ X and y ∈ Y and x ∈ (R^{⌣})^{∘}{y}.

(45) For all sets X, Y holds there exist sets x, y such that x ∈ X and y ∈ Y and x ∈ (R^{⌣})^{∘}{y} iff Y meets R^{∘}X.

(46) X misses (R^{⌣})^{∘}Y iff Y misses R^{∘}X.

(47) For every set X holds R^{∘}X = R^{∘}(X ∩ π_{1}(R)).

(48) For every set Y holds (R^{⌣})^{∘}Y = (R^{⌣})^{∘}(Y ∩ π_{2}(R)).

(49) (R[X])^{c} = (R^{c})^{∘}X.

In the sequel R denotes a relation between A and B and S denotes a relation between B and C.

Let A, B, C be sets, let R be a subset of [: A, B:], and let S be a subset of [: B, C:]. Then R · S is a relation between A and C.

One can prove the following propositions:

properties of first and second order cutting … 365

(50) (R^{∘}X)^{c} = R^{c}[X].

(51) π_{1}(R) = (R^{⌣})^{∘}B and π_{2}(R) = R^{∘}A.

(52) π_{1}(R · S) = (R^{⌣})^{∘}π_{1}(S) and π_{1}(R · S) ⊆ π_{1}(R).

(53) π_{2}(R · S) = S^{∘}π_{2}(R) and π_{2}(R · S) ⊆ π_{2}(S).

(54) X ⊆ π_{1}(R) iff X ⊆ (R · R^{⌣})^{∘}X.

(55) Y ⊆ π_{2}(R) iff Y ⊆ (R^{⌣} · R)^{∘}Y.

(56) π_{1}(R) = (R^{⌣})^{∘}B and (R^{⌣})^{∘}R^{∘}A = (R^{⌣})^{∘}π_{2}(R).

(57) (R^{⌣})^{∘}B = (R · R^{⌣})^{∘}A.

(58) R^{∘}A = (R^{⌣} · R)^{∘}B.

(59) S[R^{∘}X] = (R · S^{c})^{c}[X].

(60) (R^{c})^{⌣} = (R^{⌣})^{c}.

(61) X ⊆ R^{⌣}[Y] iff Y ⊆ R[X].

(62) R^{∘}X^{c} ⊆ Y^{c} iff (R^{⌣})^{∘}Y ⊆ X.

(63) X ⊆ R^{⌣}[R[X]] and Y ⊆ R[R^{⌣}[Y]].

(64) R[X] = R[R^{⌣}[R[X]]] and R^{⌣}[Y] = R^{⌣}[R[R^{⌣}[Y]]].

(65) id_{A} · R = R · id_{B}.

References

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

[2] Grzegorz Bancerek. Minimal signature for partial algebra. Formalized Mathematics, 5(3):405–414, 1996.

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

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

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

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

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

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

[9] Jacques Riguet. Relations binaires, fermetures, correspondances de Galois. Bulletin de la S.M.F., 76:114–155, 1948. On WWW: http://www.numdam.org/item?id=-

BSFM 1948 76 114 0.

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

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

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

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

366 krzysztof retel

The Inner Product and Conjugate of Finite Sequences of Complex Numbers

Wenpai Chang Shinshu University

Nagano, Japan Hiroshi Yamazaki Shinshu University Nagano, Japan Yatsuka Nakamura Shinshu University Nagano, Japan

Summary. The concept of “the inner product and conjugate of finite sequences of complex numbers” is defined here. Addition, subtraction, scalar multiplication and inner product are introduced using correspondent definitions of “conjugate of finite sequences of field”. Many equations for such operations consist like a case of “conjugate of finite sequences of field”. Some operations on the set of n-tuples of complex numbers are introduced as well. Additionally, difference of such n-tuples, complement of a n-tuple and multiplication of these are defined in terms of complex numbers.

      MML identifier: COMPLSP2, version: 7.5.01 4.39.921

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

1. Preliminaries

For simplicity, we adopt the following convention: i, j are natural numbers, x, y, z are finite sequences of elements of ℂ, c is an element of ℂ, and R, R_{1}, R_{2} are elements of ℂ^{i}.

Let z be a finite sequence of elements of ℂ. The functor \overline{z} yielding a finite sequence of elements of ℂ is defined by:

(Def. 1) len \overline{z} = len z and for every natural number i such that 1 ≤ i and i ≤ len z

holds \overline{z} (i) = \overline{z(i)}. The following propositions are true:

(1) If i ∈ dom(x + y), then (x + y)(i) = x(i) + y(i).

(2) If i ∈ dom(x − y), then (x − y)(i) = x(i) − y(i).

Let us consider i, R_{1}, R_{2}. Then R_{1} − R_{2} is an element of ℂ^{i}.

Let us consider i, R_{1}, R_{2}. Then R_{1} + R_{2} is an element of ℂ^{i}.

Let us consider i, let r be a complex number, and let us consider R. Then r · R is an element of ℂ^{i}.

We now state a number of propositions:

(3) For every complex number a and for every finite sequence x of elements of ℂ holds len(a · x) = len x.

(4) For every finite sequence x of elements of ℂ holds dom x = dom(−x).

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

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

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

(8) Every finite sequence f of elements of ℂ is an element of ℂ^{len f}.

(9) R_{1} − R_{2} = R_{1} + −R_{2}.

(10) For all finite sequences x, y of elements of ℂ such that len x = len y holds x − y = x + −y.

(11) (−1) · R = −R.

(12) For every finite sequence x of elements of ℂ holds (−1) · x = −x.

(13) For every finite sequence x of elements of ℂ holds (−x)(i) = −x(i). Let us consider i, R. Then −R is an element of ℂ^{i}. The following propositions are true:

(14) If c = R(j), then (−R)(j) = −c.

(15) For every complex number a holds dom(a · x) = dom x.

(16) For every complex number a holds (a · x)(i) = a · x(i).

(17) For every complex number a holds \overline{a · x} = \overline{a} · \overline{x}.

(18) (R_{1} + R_{2})(j) = R_{1}(j) + R_{2}(j).

(19) For all finite sequences x_{1}, x_{2} of elements of ℂ such that len x_{1} = len x_{2} holds \overline{x_{1} + x_{2}} = \overline{x_{1}} + \overline{x_{2}} .

(20) (R_{1} − R_{2})(j) = R_{1}(j) − R_{2}(j).

(21) For all finite sequences x_{1}, x_{2} of elements of ℂ such that len x_{1} = len x_{2} holds \overline{x_{1} − x_{2}} = \overline{x_{1}} − \overline{x_{2}} .

(22) For every finite sequence z of elements of ℂ holds \overline{\overline{z}} = z.

(23) For every finite sequence z of elements of ℂ holds \overline{−z} = −\overline{z} .

(24) For every complex number z holds z + \overline{z} = 2 · ℜ(z).

(25) For all finite sequences x, y of elements of ℂ such that len x = len y holds (x − y)(i) = x(i) − y(i).

(26) For all finite sequences x, y of elements of ℂ such that len x = len y holds

(x + y)(i) = x(i) + y(i). Let z be a finite sequence of elements of ℂ. The functor ℜ(z) yields a finite

sequence of elements of ℝ and is defined as follows: (Def. 2) ℜ(z) = \frac{1}{2} · (z + \overline{z}).

One can prove the following proposition

(27) For every complex number z holds z − \overline{z} = 2 · ℑ(z) · i.

Let z be a finite sequence of elements of ℂ. The functor ℑ(z) yielding a finite sequence of elements of ℝ is defined as follows:

(Def. 3) ℑ(z) = (−\frac{1}{2} · i) · (z − \overline{z}).

Let x, y be finite sequences of elements of ℂ. The functor |(x, y)| yields an element of ℂ and is defined by:

(Def. 4) |(x, y)| = (|(ℜ(x), ℜ(y))| − i · |(ℜ(x), ℑ(y))|) + i · |(ℑ(x), ℜ(y))| +

|(ℑ(x), ℑ(y))|. We now state four propositions:

(28) For all finite sequences x, y, z of elements of ℂ such that len x = len y and len y = len z holds x + (y + z) = (x + y) + z.

(29) For all finite sequences x, y of elements of ℂ such that len x = len y holds x + y = y + x.

(30) Let c be a complex number and x, y be finite sequences of elements of ℂ. If len x = len y, then c · (x + y) = c · x + c · y.

(31) For all finite sequences x, y of elements of ℂ such that len x = len y holds

x − y = x + −y. Let us consider i, c. Then i ↦ c is an element of ℂ^{i}. Next we state a number of propositions:

(32) For all finite sequences x, y of elements of ℂ such that len x = len y and x + y = 0_{ℂ}^{len x} holds x = −y and y = −x.

(33) For every finite sequence x of elements of ℂ holds x + 0_{ℂ}^{len x} = x.

(34) For every finite sequence x of elements of ℂ holds x + −x = 0_{ℂ}^{len x}.

(35) For all finite sequences x, y of elements of ℂ such that len x = len y holds −(x + y) = −x + −y.

(36) For all finite sequences x, y, z of elements of ℂ such that len x = len y and len y = len z holds x − y − z = x − (y + z).

(37) For all finite sequences x, y, z of elements of ℂ such that len x = len y and len y = len z holds x + (y − z) = (x + y) − z.

(38) For every finite sequence x of elements of ℂ holds −−x = x.

(39) For all finite sequences x, y of elements of ℂ such that len x = len y holds −(x − y) = −x + y.

(40) For all finite sequences x, y, z of elements of ℂ such that len x = len y and len y = len z holds x − (y − z) = (x − y) + z.

(41) For every complex number c holds c · 0_{ℂ}^{len x} = 0_{ℂ}^{len x}.

(42) For every complex number c holds −c · x = c · −x.

(43) Let c be a complex number and x, y be finite sequences of elements of ℂ. If len x = len y, then c · (x − y) = c · x − c · y.

(44) For all elements x_{1}, y_{1} of ℂ and for all real numbers x_{2}, y_{2} such that

x_{1} = x_{2} and y_{1} = y_{2} holds +_{ℂ}(x_{1}, y_{1}) = +_{ℝ}(x_{2}, y_{2}). In the sequel C is a function from [: ℂ, ℂ:] into ℂ and G is a function from

[: ℝ, ℝ:] into ℝ.

One can prove the following proposition

(45) Let x_{1}, y_{1} be finite sequences of elements of ℂ and x_{2}, y_{2} be finite sequences of elements of ℝ. Suppose x_{1} = x_{2} and y_{1} = y_{2} and len x_{1} = len y_{2} and for every i such that i ∈ dom x_{1} holds C(x_{1}(i), y_{1}(i)) = G(x_{2}(i), y_{2}(i)). Then C^{∘}(x_{1}, y_{1}) = G^{∘}(x_{2}, y_{2}).

Let z be a finite sequence of elements of ℝ and let i be a set. Then z(i) is an element of ℝ.

We now state several propositions:

(46) Let x_{1}, y_{1} be finite sequences of elements of ℂ and x_{2}, y_{2} be finite sequences of elements of ℝ. If x_{1} = x_{2} and y_{1} = y_{2} and len x_{1} = len y_{2}, then (+_{ℂ})^{∘}(x_{1}, y_{1}) = (+_{ℝ})^{∘}(x_{2}, y_{2}).

(47) Let x_{1}, y_{1} be finite sequences of elements of ℂ and x_{2}, y_{2} be finite sequences of elements of ℝ. If x_{1} = x_{2} and y_{1} = y_{2} and len x_{1} = len y_{2}, then x_{1} + y_{1} = x_{2} + y_{2}.

(48) For every finite sequence x of elements of ℂ holds len ℜ(x) = len x and len ℑ(x) = len x.

(49) For all finite sequences x, y of elements of ℂ such that len x = len y holds ℜ(x + y) = ℜ(x) + ℜ(y) and ℑ(x + y) = ℑ(x) + ℑ(y).

(50) Let x_{1}, y_{1} be finite sequences of elements of ℂ and x_{2}, y_{2} be finite sequences of elements of ℝ. If x_{1} = x_{2} and y_{1} = y_{2} and len x_{1} = len y_{2}, then (−_{ℂ})^{∘}(x_{1}, y_{1}) = (−_{ℝ})^{∘}(x_{2}, y_{2}).

(51) Let x_{1}, y_{1} be finite sequences of elements of ℂ and x_{2}, y_{2} be finite sequences of elements of ℝ. If x_{1} = x_{2} and y_{1} = y_{2} and len x_{1} = len y_{2}, then x_{1} − y_{1} = x_{2} − y_{2}.

(52) For all finite sequences x, y of elements of ℂ such that len x = len y holds ℜ(x − y) = ℜ(x) − ℜ(y) and ℑ(x − y) = ℑ(x) − ℑ(y).

(53) For all complex numbers a, b holds a · (b · z) = (a · b) · z.

(54) For every complex number c holds (−c) · x = −c · x.

In the sequel h is a function from ℂ into ℂ and g is a function from ℝ into ℝ.

One can prove the following propositions:

(55) Let y_{1} be a finite sequence of elements of ℂ and y_{2} be a finite sequence of elements of ℝ. If len y_{1} = len y_{2} and for every i such that i ∈ dom y_{1} holds h(y_{1}(i)) = g(y_{2}(i)), then h · y_{1} = g · y_{2}.

(56) Let y_{1} be a finite sequence of elements of ℂ and y_{2} be a finite sequence of elements of ℝ. If y_{1} = y_{2} and len y_{1} = len y_{2}, then −_{ℂ} · y_{1} = −_{ℝ} · y_{2}.

(57) Let y_{1} be a finite sequence of elements of ℂ and y_{2} be a finite sequence of elements of ℝ. If y_{1} = y_{2} and len y_{1} = len y_{2}, then −y_{1} = −y_{2}.

(58) For every finite sequence x of elements of ℂ holds ℜ(i · x) = −ℑ(x) and ℑ(i · x) = ℜ(x).

(59) For all finite sequences x, y of elements of ℂ such that len x = len y holds |(i · x, y)| = i · |(x, y)|.

(60) For all finite sequences x, y of elements of ℂ such that len x = len y holds |(x, i · y)| = −i · |(x, y)|.

(61) Let a_{1} be an element of ℂ, y_{1} be a finite sequence of elements of ℂ, a_{2} be an element of ℝ, and y_{2} be a finite sequence of elements of ℝ. If a_{1} = a_{2} and y_{1} = y_{2} and len y_{1} = len y_{2}, then ·_{ℂ}^{(a_{1})} ·y_{1} = ·_{ℝ}^{a_{2}} ·y_{2}.

(62) Let a_{1} be a complex number, y_{1} be a finite sequence of elements of ℂ, a_{2} be an element of ℝ, and y_{2} be a finite sequence of elements of ℝ. If a_{1} = a_{2} and y_{1} = y_{2} and len y_{1} = len y_{2}, then a_{1} · y_{1} = a_{2} · y_{2}.

(63) For all complex numbers a, b holds (a + b) · z = a · z + b · z.

(64) For all complex numbers a, b holds (a − b) · z = a · z − b · z.

(65) Let a be an element of ℂ and x be a finite sequence of elements of ℂ. Then ℜ(a · x) = ℜ(a) · ℜ(x) − ℑ(a) · ℑ(x) and ℑ(a · x) = ℑ(a) · ℜ(x) + ℜ(a) · ℑ(x).

2. The Inner Product and Conjugate of Finite Sequences

The following propositions are true:

(66) For all finite sequences x_{1}, x_{2}, y of elements of ℂ such that len x_{1} = len x_{2} and len x_{2} = len y holds |(x_{1} + x_{2}, y)| = |(x_{1}, y)| + |(x_{2}, y)|.

(67) For all finite sequences x_{1}, x_{2} of elements of ℂ such that len x_{1} = len x_{2} holds |(−x_{1}, x_{2})| = −|(x_{1}, x_{2})|.

(68) For all finite sequences x_{1}, x_{2} of elements of ℂ such that len x_{1} = len x_{2} holds |(x_{1}, −x_{2})| = −|(x_{1}, x_{2})|.

(69) For all finite sequences x_{1}, x_{2} of elements of ℂ such that len x_{1} = len x_{2} holds |(−x_{1}, −x_{2})| = |(x_{1}, x_{2})|.

(70) For all finite sequences x_{1}, x_{2}, x_{3} of elements of ℂ such that len x_{1} = len x_{2} and len x_{2} = len x_{3} holds |(x_{1} − x_{2}, x_{3})| = |(x_{1}, x_{3})| − |(x_{2}, x_{3})|.

(71) For all finite sequences x, y_{1}, y_{2} of elements of ℂ such that len x = len y_{1} and len y_{1} = len y_{2} holds |(x, y_{1} + y_{2})| = |(x, y_{1})| + |(x, y_{2})|.

(72) For all finite sequences x, y_{1}, y_{2} of elements of ℂ such that len x = len y_{1} and len y_{1} = len y_{2} holds |(x, y_{1} − y_{2})| = |(x, y_{1})| − |(x, y_{2})|.

(73) Let x_{1}, x_{2}, y_{1}, y_{2} be finite sequences of elements of ℂ. If len x_{1} = len x_{2} and len x_{2} = len y_{1} and len y_{1} = len y_{2}, then |(x_{1}+x_{2}, y_{1}+y_{2})| = |(x_{1}, y_{1})|+ |(x_{1}, y_{2})| + |(x_{2}, y_{1})| + |(x_{2}, y_{2})|.

(74) Let x_{1}, x_{2}, y_{1}, y_{2} be finite sequences of elements of ℂ. If len x_{1} = len x_{2} and len x_{2} = len y_{1} and len y_{1} = len y_{2}, then |(x_{1} − x_{2}, y_{1} − y_{2})| = (|(x_{1}, y_{1})| − |(x_{1}, y_{2})| − |(x_{2}, y_{1})|) + |(x_{2}, y_{2})|.

(75) For all finite sequences x, y of elements of ℂ such that len x = len y holds |(x, y)| = \overline{|(y, x)|}.

(76) For all finite sequences x, y of elements of ℂ such that len x = len y holds |(x + y, x + y)| = |(x, x)| + 2 · ℜ(|(x, y)|) + |(y, y)|.

(77) For all finite sequences x, y of elements of ℂ such that len x = len y holds |(x − y, x − y)| = (|(x, x)| − 2 · ℜ(|(x, y)|)) + |(y, y)|.

(78) For every element a of ℂ and for all finite sequences x, y of elements of ℂ such that len x = len y holds |(a · x, y)| = a · |(x, y)|.

(79) For every element a of ℂ and for all finite sequences x, y of elements of ℂ such that len x = len y holds |(x, a · y)| = \overline{a} · |(x, y)|.

(80) Let a, b be elements of ℂ and x, y, z be finite sequences of elements of ℂ. If len x = len y and len y = len z, then |(a·x+b·y, z)| = a·|(x, z)|+b·|(y, z)|.

(81) Let a, b be elements of ℂ and x, y, z be finite sequences of elements of ℂ. If len x = len y and len y = len z, then |(x, a·y+b·z)| = \overline{a}·|(x, y)|+\overline{b}·|(x, z)|.

References

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

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

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

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

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

[6] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 1990.

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

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

the inner product and conjugate of finite … 373

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

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

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

[12] Czesław Byliński and Andrzej Trybulec. Complex spaces. Formalized Mathematics, 2(1):151–158, 1991.

[13] Wenpai Chang, Hiroshi Yamazaki, and Yatsuka Nakamura. A theory of matrices of complex elements. Formalized Mathematics, 13(1):157–162, 2005.

[14] Library Committee of the Association of Mizar Users. Binary operations on numbers. To appear in Formalized Mathematics.

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

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

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

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

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

374 wenpai chang et al.

Inferior Limit and Superior Limit of Sequences of Real Numbers

Bo Zhang Shinshu University

Nagano, Japan Hiroshi Yamazaki Shinshu University Nagano, Japan Yatsuka Nakamura Shinshu University Nagano, Japan

Summary. The concept of inferior limit and superior limit of sequences of real numbers is defined here. This article contains the following items: definition of the superior sequence and the inferior sequence of real numbers, definition of the superior limit and the inferior limit of real number, and definition of the relation between the limit value and the superior limit, the inferior limit of sequences of real numbers.

      MML identifier: RINFSUP1, version: 7.5.01 4.39.921

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

We adopt the following rules: n, m, k denote natural numbers, r, s, t denote real numbers, and s_{1}, s_{2}, s_{3} denote sequences of real numbers.

One can prove the following proposition

(1) s − r < t and s + r > t iff |t − s| < r.

Let s_{1} be a sequence of real numbers. The functor sup s_{1} yielding a real number is defined by:

(Def. 1) sup s_{1} = sup rng s_{1}.

Let s_{1} be a sequence of real numbers. The functor inf s_{1} yielding a real number is defined as follows:

(Def. 2) inf s_{1} = inf rng s_{1}. The following propositions are true:

(2) (s_{2} + s_{3}) − s_{3} = s_{2}.

(3) r ∈ rng s_{1} iff −r ∈ rng(−s_{1}).

(4) rng(−s_{1}) = −rng s_{1}.

(5) s_{1} is upper bounded iff rng s_{1} is upper bounded.

(6) s_{1} is lower bounded iff rng s_{1} is lower bounded.

(7) Suppose s_{1} is upper bounded. Then r = sup s_{1} if and only if the following conditions are satisfied:

(i) for every n holds s_{1}(n) ≤ r, and (ii) for every s such that 0 < s there exists k such that r − s < s_{1}(k).

(8) Suppose s_{1} is lower bounded. Then r = inf s_{1} if and only if the following conditions are satisfied:

(i) for every n holds r ≤ s_{1}(n), and (ii) for every s such that 0 < s there exists k such that s_{1}(k) < r + s.

(9) For every n holds s_{1}(n) ≤ r iff s_{1} is upper bounded and sup s_{1} ≤ r.

(10) For every n holds r ≤ s_{1}(n) iff s_{1} is lower bounded and r ≤ inf s_{1}.

(11) s_{1} is upper bounded iff −s_{1} is lower bounded.

(12) s_{1} is lower bounded iff −s_{1} is upper bounded.

(13) If s_{1} is upper bounded, then sup s_{1} = −inf(−s_{1}).

(14) If s_{1} is lower bounded, then inf s_{1} = −sup(−s_{1}).

(15) If s_{2} is lower bounded and s_{3} is lower bounded, then inf(s_{2} + s_{3}) ≥ inf s_{2} + inf s_{3}.

(16) If s_{2} is upper bounded and s_{3} is upper bounded, then sup(s_{2} + s_{3}) ≤

sup s_{2} + sup s_{3}. Let f be a sequence of real numbers. We introduce f is non-negative as a

synonym of f is non-negative yielding.

Let f be a sequence of real numbers. Let us observe that f is non-negative if and only if:

(Def. 3) For every n holds f(n) ≥ 0.

The following propositions are true:

(17) If s_{1} is non-negative, then s_{1} ↑ k is non-negative.

(18) If s_{1} is lower bounded and non-negative, then inf s_{1} ≥ 0.

(19) If s_{1} is upper bounded and non-negative, then sup s_{1} ≥ 0.

(20) Suppose s_{2} is lower bounded and non-negative and s_{3} is lower bounded and non-negative. Then s_{2} s_{3} is lower bounded and inf(s_{2} s_{3}) ≥ inf s_{2} · inf s_{3}.

(21) Suppose s_{2} is upper bounded and non-negative and s_{3} is upper bounded and non-negative. Then s_{2} s_{3} is upper bounded and sup(s_{2} s_{3}) ≤ sup s_{2} · sup s_{3}.

(22) If s_{1} is non-decreasing and upper bounded, then s_{1} is bounded.

(23) If s_{1} is non-increasing and lower bounded, then s_{1} is bounded.

(24) If s_{1} is non-decreasing and upper bounded, then lim s_{1} = sup s_{1}.

(25) If s_{1} is non-increasing and lower bounded, then lim s_{1} = inf s_{1}.

(26) If s_{1} is upper bounded, then s_{1} ↑ k is upper bounded.

(27) If s_{1} is lower bounded, then s_{1} ↑ k is lower bounded.

(28) If s_{1} is bounded, then s_{1} ↑ k is bounded.

(29) For all s_{1}, n holds {s_{1}(k) : n ≤ k} is a subset of ℝ.

(30) rng(s_{1} ↑ k) = {s_{1}(n) : k ≤ n}.

(31) If s_{1} is upper bounded, then for every n and for every subset R of ℝ such that R = {s_{1}(k) : n ≤ k} holds R is upper bounded.

(32) If s_{1} is lower bounded, then for every n and for every subset R of ℝ such that R = {s_{1}(k) : n ≤ k} holds R is lower bounded.

(33) If s_{1} is bounded, then for every n and for every subset R of ℝ such that R = {s_{1}(k) : n ≤ k} holds R is bounded.

(34) If s_{1} is non-decreasing, then for every n and for every subset R of ℝ such that R = {s_{1}(k) : n ≤ k} holds inf R = s_{1}(n).

(35) If s_{1} is non-increasing, then for every n and for every subset R of ℝ such that R = {s_{1}(k) : n ≤ k} holds sup R = s_{1}(n).

(36) Let given s_{1}. Then there exists a function f from ℕ into ℝ such that for every n and for every subset Y of ℝ if Y = {s_{1}(k) : n ≤ k}, then f(n) = sup Y.

(37) Let given s_{1}. Then there exists a function f from ℕ into ℝ such that for every n and for every subset Y of ℝ if Y = {s_{1}(k) : n ≤ k}, then f(n) = inf Y.

Let s_{1} be a sequence of real numbers. The inferior realsequence s_{1} yields a sequence of real numbers and is defined as follows:

(Def. 4) For every n and for every subset Y of ℝ such that Y = {s_{1}(k) : n ≤ k}

holds (the inferior realsequence s_{1})(n) = inf Y. Let s_{1} be a sequence of real numbers. The superior realsequence s_{1} yields a

sequence of real numbers and is defined by: (Def. 5) For every n and for every subset Y of ℝ such that Y = {s_{1}(k) : n ≤ k}

holds (the superior realsequence s_{1})(n) = sup Y. Next we state a number of propositions:

(38) (The inferior realsequence s_{1})(n) = inf(s_{1} ↑ n).

(39) (The superior realsequence s_{1})(n) = sup(s_{1} ↑ n).

(40) If s_{1} is lower bounded, then (the inferior realsequence s_{1})(0) = inf s_{1}.

(41) If s_{1} is upper bounded, then (the superior realsequence s_{1})(0) = sup s_{1}.

(42) Suppose s_{1} is lower bounded. Then r = (the inferior realsequence s_{1})(n) if and only if for every k holds r ≤ s_{1}(n + k) and for every s such that 0 < s there exists k such that s_{1}(n + k) < r + s.

(43) Suppose s_{1} is upper bounded. Then r = (the superior realsequence s_{1})(n) if and only if for every k holds s_{1}(n + k) ≤ r and for every s such that 0 < s there exists k such that r − s < s_{1}(n + k).

(44) If s_{1} is lower bounded, then for every k holds r ≤ s_{1}(n + k) iff r ≤ (the inferior realsequence s_{1})(n).

(45) Suppose s_{1} is lower bounded. Then for every m such that n ≤ m holds r ≤ s_{1}(m) if and only if r ≤ (the inferior realsequence s_{1})(n).

(46) If s_{1} is upper bounded, then for every k holds s_{1}(n + k) ≤ r iff (the superior realsequence s_{1})(n) ≤ r.

(47) Suppose s_{1} is upper bounded. Then for every m such that n ≤ m holds s_{1}(m) ≤ r if and only if (the superior realsequence s_{1})(n) ≤ r.

(48) If s_{1} is lower bounded, then (the inferior realsequence s_{1})(n) = min((the inferior realsequence s_{1})(n + 1), s_{1}(n)).

(49) If s_{1} is upper bounded, then (the superior realsequence s_{1})(n) = max((the superior realsequence s_{1})(n + 1), s_{1}(n)).

(50) If s_{1} is lower bounded, then (the inferior realsequence s_{1})(n) ≤ (the inferior realsequence s_{1})(n + 1).

(51) If s_{1} is upper bounded, then (the superior realsequence s_{1})(n+1) ≤ (the superior realsequence s_{1})(n).

(52) If s_{1} is lower bounded, then the inferior realsequence s_{1} is non-decreasing.

(53) If s_{1} is upper bounded, then the superior realsequence s_{1} is nonincreasing.

(54) If s_{1} is bounded, then (the inferior realsequence s_{1})(n) ≤ (the superior realsequence s_{1})(n).

(55) If s_{1} is bounded, then (the inferior realsequence s_{1})(n) ≤ inf (the superior realsequence s_{1}).

(56) If s_{1} is bounded, then sup (the inferior realsequence s_{1}) ≤ (the superior realsequence s_{1})(n).

(57) If s_{1} is bounded, then sup (the inferior realsequence s_{1}) ≤ inf (the superior realsequence s_{1}).

(58) If s_{1} is bounded, then the superior realsequence s_{1} is bounded and the inferior realsequence s_{1} is bounded.

(59) Suppose s_{1} is bounded. Then (i) the inferior realsequence s_{1} is convergent, and (ii) lim (the inferior realsequence s_{1}) = sup (the inferior realsequence s_{1}).

(60) Suppose s_{1} is bounded. Then (i) the superior realsequence s_{1} is convergent, and (ii) lim (the superior realsequence s_{1}) = inf (the superior realsequence s_{1}).

(61) If s_{1} is lower bounded, then (the inferior realsequence s_{1})(n) = −(the superior realsequence −s_{1})(n).

(62) If s_{1} is upper bounded, then (the superior realsequence s_{1})(n) = −(the inferior realsequence −s_{1})(n).

(63) If s_{1} is lower bounded, then the inferior realsequence s_{1} = −the superior realsequence −s_{1}.

(64) If s_{1} is upper bounded, then the superior realsequence s_{1} = −the inferior realsequence −s_{1}.

(65) If s_{1} is non-decreasing, then s_{1}(n) ≤ (the inferior realsequence s_{1})(n+1).

(66) If s_{1} is non-decreasing, then the inferior realsequence s_{1} = s_{1}.

(67) If s_{1} is non-decreasing and upper bounded, then s_{1}(n) ≤ (the superior realsequence s_{1})(n + 1).

(68) Suppose s_{1} is non-decreasing and upper bounded. Then (the superior realsequence s_{1})(n) = (the superior realsequence s_{1})(n + 1).

(69) Suppose s_{1} is non-decreasing and upper bounded. Then (the superior realsequence s_{1})(n) = sup s_{1} and the superior realsequence s_{1} is constant.

(70) If s_{1} is non-decreasing and upper bounded, then inf (the superior realsequence s_{1}) = sup s_{1}.

(71) If s_{1} is non-increasing, then (the superior realsequence s_{1})(n+1) ≤ s_{1}(n).

(72) If s_{1} is non-increasing, then the superior realsequence s_{1} = s_{1}.

(73) If s_{1} is non-increasing and lower bounded, then (the inferior realsequence s_{1})(n + 1) ≤ s_{1}(n).

(74) Suppose s_{1} is non-increasing and lower bounded. Then (the inferior realsequence s_{1})(n) = (the inferior realsequence s_{1})(n + 1).

(75) Suppose s_{1} is non-increasing and lower bounded. Then (the inferior realsequence s_{1})(n) = inf s_{1} and the inferior realsequence s_{1} is constant.

(76) If s_{1} is non-increasing and lower bounded, then sup (the inferior realsequence s_{1}) = inf s_{1}.

(77) Suppose s_{2} is bounded and s_{3} is bounded and for every n holds s_{2}(n) ≤

s_{3}(n). Then

(i) for every n holds (the superior realsequence s_{2})(n) ≤ (the superior realsequence s_{3})(n), and

(ii) for every n holds (the inferior realsequence s_{2})(n) ≤ (the inferior re-

alsequence s_{3})(n).

(78) Suppose s_{2} is lower bounded and s_{3} is lower bounded. Then (the inferior realsequence s_{2} + s_{3})(n) ≥ (the inferior realsequence s_{2})(n) + (the inferior realsequence s_{3})(n).

(79) Suppose s_{2} is upper bounded and s_{3} is upper bounded. Then (the superior realsequence s_{2} + s_{3})(n) ≤ (the superior realsequence s_{2})(n) + (the

superior realsequence s_{3})(n).

(80) Suppose s_{2} is lower bounded and non-negative and s_{3} is lower bounded and non-negative. Then (the inferior realsequence s_{2} s_{3})(n) ≥ (the inferior realsequence s_{2})(n) · (the inferior realsequence s_{3})(n).

(81) Suppose s_{2} is lower bounded and non-negative and s_{3} is lower bounded and non-negative. Then (the inferior realsequence s_{2} s_{3})(n) ≥ (the inferior realsequence s_{2})(n) · (the inferior realsequence s_{3})(n).

(82) Suppose s_{2} is upper bounded and non-negative and s_{3} is upper bounded and non-negative. Then (the superior realsequence s_{2} s_{3})(n) ≤ (the superior realsequence s_{2})(n) · (the superior realsequence s_{3})(n).

Let s_{1} be a sequence of real numbers. The functor lim sup s_{1} yielding an element of ℝ is defined as follows:

(Def. 6) lim sup s_{1} = inf (the superior realsequence s_{1}).

Let s_{1} be a sequence of real numbers. The functor lim inf s_{1} yielding an element of ℝ is defined by:

(Def. 7) lim inf s_{1} = sup (the inferior realsequence s_{1}).

Next we state a number of propositions:

(83) If s_{1} is bounded, then lim inf s_{1} ≤ r iff for every s such that 0 < s and for every n there exists k such that s_{1}(n + k) < r + s.

(84) If s_{1} is bounded, then r ≤ lim inf s_{1} iff for every s such that 0 < s there exists n such that for every k holds r − s < s_{1}(n + k).

(85) Suppose s_{1} is bounded. Then r = lim inf s_{1} if and only if for every s such that 0 < s holds for every n there exists k such that s_{1}(n+k) < r +s and there exists n such that for every k holds r − s < s_{1}(n + k).

(86) If s_{1} is bounded, then r ≤ lim sup s_{1} iff for every s such that 0 < s and for every n there exists k such that s_{1}(n + k) > r − s.

(87) If s_{1} is bounded, then lim sup s_{1} ≤ r iff for every s such that 0 < s there exists n such that for every k holds s_{1}(n + k) < r + s.

(88) Suppose s_{1} is bounded. Then r = lim sup s_{1} if and only if for every s such that 0 < s holds for every n there exists k such that s_{1}(n+k) > r −s and there exists n such that for every k holds s_{1}(n + k) < r + s.

(89) If s_{1} is bounded, then lim inf s_{1} ≤ lim sup s_{1}.

(90) s_{1} is bounded and lim sup s_{1} = lim inf s_{1} iff s_{1} is convergent.

(91) If s_{1} is convergent, then lim s_{1} = lim sup s_{1} and lim s_{1} = lim inf s_{1}.

(92) If s_{1} is bounded, then lim sup(−s_{1}) = −lim inf s_{1} and lim inf(−s_{1}) = −lim sup s_{1}.

(93) If s_{2} is bounded and s_{3} is bounded and for every n holds s_{2}(n) ≤ s_{3}(n), then lim sup s_{2} ≤ lim sup s_{3} and lim inf s_{2} ≤ lim inf s_{3}.

inferior limit and superior limit … 381

(94) Suppose s_{2} is bounded and s_{3} is bounded. Then lim inf s_{2} + lim inf s_{3} ≤ lim inf(s_{2}+s_{3}) and lim inf(s_{2}+s_{3}) ≤ lim inf s_{2}+lim sup s_{3} and lim inf(s_{2}+ s_{3}) ≤ lim sup s_{2}+lim inf s_{3} and lim inf s_{2}+lim sup s_{3} ≤ lim sup(s_{2}+s_{3}) and lim sup s_{2} +lim inf s_{3} ≤ lim sup(s_{2} +s_{3}) and lim sup(s_{2} +s_{3}) ≤ lim sup s_{2} + lim sup s_{3} and if s_{2} is convergent or s_{3} is convergent, then lim inf(s_{2}+s_{3}) = lim inf s_{2} + lim inf s_{3} and lim sup(s_{2} + s_{3}) = lim sup s_{2} + lim sup s_{3}.

(95) If s_{2} is bounded and non-negative and s_{3} is bounded and non-negative, then lim inf s_{2} · lim inf s_{3} ≤ lim inf(s_{2} s_{3}) and lim sup(s_{2} s_{3}) ≤ lim sup s_{2} · lim sup s_{3}.

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] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 1990.

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

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

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

[7] Artur Korniłowicz. On the real valued functions. Formalized Mathematics, 13(1):181–187, 2005.

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

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

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

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

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

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

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

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

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

382 bo zhang et al.

Formulas and Identities of Inverse Hyperbolic Functions

Fuguo Ge

Qingdao University of Science

and Technology China

Xiquan Liang Qingdao University of Science and Technology China

Yuzhong Ding Qingdao University of Science and Technology China

Summary. This article describes definitions of inverse hyperbolic functions and their main properties, as well as some addition formulas with hyperbolic functions.

MML identifier: SIN COS7, version: 7.5.01 4.39.921

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

1. Preliminaries

In this paper x, y, t denote real numbers. Next we state a number of propositions:

(1) If x > 0, then \frac{1}{x} = x^{−1}.

(2) If x > 1, then (\frac{\sqrt{x^{2}−1}}{x})^{2} < 1.

(3) (\frac{x}{\sqrt{x^{2}+1}})^{2} < 1.

(4) \sqrt{x^{2} + 1} > 0.

(5) \sqrt{x^{2} + 1} + x > 0.

(6) If y ≥ 0 and x ≥ 1, then \frac{x+1}{y} ≥ 0.

(7) If y ≥ 0 and x ≥ 1, then \frac{x−1}{y} ≥ 0.

(8) If x ≥ 1, then \sqrt{\frac{x+1}{2}} ≥ 1.

(9) If y ≥ 0 and x ≥ 1, then \frac{x^{2}−1}{y} ≥ 0.

(10) If x ≥ 1, then \sqrt{\frac{x+1}{2}} + \sqrt{\frac{x−1}{2}} > 0.

(11) If x^{2} < 1, then x + 1 > 0 and 1 − x > 0.

(12) If x ≠ 1, then (1 − x)^{2} > 0.

(13) If x^{2} < 1, then \frac{x^{2}+1}{1−x^{2}} ≥ 0.

(14) If x^{2} < 1, then (\frac{2·x}{1+x^{2}} )^{2} < 1.

(15) If 0 < x and x < 1, then \frac{1+x}{1−x} > 0.

(16) If 0 < x and x < 1, then x^{2} < 1.

(17) If 0 < x and x < 1, then \frac{1}{\sqrt{1−x^{2}}} > 1.

(18) If 0 < x and x < 1, then \frac{2·x}{1−x^{2}} > 0.

(19) If 0 < x and x < 1, then 0 < (1 − x^{2})^{2}.

(20) If 0 < x and x < 1, then \frac{1+x^{2}}{1−x^{2}} > 1.

(21) If 1 < x^{2}, then (\frac{1}{x})^{2} < 1.

(22) If 0 < x and x ≤ 1, then 1 − x^{2} ≥ 0.

(23) If 1 ≤ x, then 0 < x + \sqrt{x^{2} − 1}.

(24) If 1 ≤ x and 1 ≤ y, then 0 ≤ x · \sqrt{y^{2} − 1} + y · \sqrt{x^{2} − 1}.

(25) If 1 ≤ x and 1 ≤ y and |y| ≤ |x|, then 0 < y − \sqrt{y^{2} − 1}.

(26) If 1 ≤ x and 1 ≤ y and |y| ≤ |x|, then 0 ≤ y · \sqrt{x^{2} − 1} − x · \sqrt{y^{2} − 1}.

(27) If x^{2} < 1 and y^{2} < 1, then x · y ≠ −1.

(28) If x^{2} < 1 and y^{2} < 1, then x · y ≠ 1.

(29) If x ≠ 0, then exp x ≠ 1.

(30) If 0 ≠ x, then (exp x)^{2} − 1 ≠ 0.

(31) If 0 < t, then \frac{t^{2}−1}{t^{2}+1} < 1.

(32) If −1 < t and t < 1, then 0 < \frac{t+1}{1−t}.

2. Formulas and Identities of Inverse Hyperbolic Functions

Let x be a real number. The functor sinh′ x yields a real number and is defined by:

(Def. 1) sinh′ x = log_{e}(x + \sqrt{x^{2} + 1}).

Let x be a real number. The functor cosh′_{1} x yielding a real number is defined by:

(Def. 2) cosh′_{1} x = log_{e}(x + \sqrt{x^{2} − 1}).

Let x be a real number. The functor cosh′_{2} x yields a real number and is defined by:

(Def. 3) cosh′_{2} x = −log_{e}(x + \sqrt{x^{2} − 1}).

Let x be a real number. The functor tanh′ x yields a real number and is defined by:

(Def. 4) tanh′ x = \frac{1}{2} · log_{e}(\frac{1+x}{1−x}).

Let x be a real number. The functor coth′ x yielding a real number is defined as follows:

(Def. 5) coth′ x = \frac{1}{2} · log_{e}(\frac{x+1}{x−1}).

Let x be a real number. The functor sech′_{1} x yields a real number and is defined by:

(Def. 6) sech′_{1} x = log_{e}(\frac{1+\sqrt{1−x^{2}}}{x}).

Let x be a real number. The functor sech′_{2} x yielding a real number is defined as follows:

(Def. 7) sech′_{2} x = −log_{e}(\frac{1+\sqrt{1−x^{2}}}{x}).

Let x be a real number. The functor csch′ x yielding a real number is defined by:

(Def. 8)(i) csch′ x = log_{e}(\frac{1+\sqrt{1+x^{2}}}{x}) if 0 < x, (ii) csch′ x = log_{e}(\frac{1−\sqrt{1+x^{2}}}{x}) if x < 0, (iii) x < 0, otherwise. The following propositions are true:

(33) If 0 ≤ x, then sinh′ x = cosh′_{1} \sqrt{x^{2} + 1}.

(34) If x < 0, then sinh′ x = cosh′_{2} \sqrt{x^{2} + 1}.

(35) sinh′ x = tanh′(\frac{x}{\sqrt{x^{2}+1}}).

(36) If x ≥ 1, then cosh′_{1} x = sinh′ \sqrt{x^{2} − 1}.

(37) If x > 1, then cosh′_{1} x = tanh′(\frac{\sqrt{x^{2}−1}}{x}).

(38) If x ≥ 1, then cosh′_{1} x = 2 · cosh′_{1} \sqrt{\frac{x+1}{2}}.

(39) If x ≥ 1, then cosh′_{2} x = 2 · cosh′_{2} \sqrt{\frac{x+1}{2}}.

(40) If x ≥ 1, then cosh′_{1} x = 2 · sinh′ \sqrt{\frac{x−1}{2}}.

(41) If x^{2} < 1, then tanh′ x = sinh′(\frac{x}{\sqrt{1−x^{2}}} ).

(42) If 0 < x and x < 1, then tanh′ x = cosh′_{1}(\frac{1}{\sqrt{1−x^{2}}} ).

(43) If x^{2} < 1, then tanh′ x = \frac{1}{2} · sinh′(\frac{2·x}{1−x^{2}} ).

(44) If x > 0 and x < 1, then tanh′ x = \frac{1}{2} · cosh′_{1}(\frac{1+x^{2}}{1−x^{2}} ).

(45) If x^{2} < 1, then tanh′ x = \frac{1}{2} · tanh′(\frac{2·x}{1+x^{2}} ).

(46) If x^{2} > 1, then coth′ x = tanh′(\frac{1}{x}).

(47) If x > 0 and x ≤ 1, then sech′_{1} x = cosh′_{1}(\frac{1}{x}).

(48) If x > 0 and x ≤ 1, then sech′_{2} x = cosh′_{2}(\frac{1}{x}).

(49) If x > 0, then csch′ x = sinh′(\frac{1}{x}).

(50) If x·y+\sqrt{x^{2} + 1}·\sqrt{y^{2} + 1} ≥ 0, then sinh′ x+sinh′ y = sinh′(x·\sqrt{1 + y^{2}}+ y · \sqrt{1 + x^{2}}).

(51) sinh′ x − sinh′ y = sinh′(x · \sqrt{1 + y^{2}} − y · \sqrt{1 + x^{2}}).

(52) If 1 ≤ x and 1 ≤ y, then cosh′_{1} x + cosh′_{1} y = cosh′_{1}(x · y + \sqrt{(x^{2} − 1) · (y^{2} − 1)}).

(53) If 1 ≤ x and 1 ≤ y, then cosh′_{2} x + cosh′_{2} y = cosh′_{2}(x · y + \sqrt{(x^{2} − 1) · (y^{2} − 1)}).

(54) If 1 ≤ x and 1 ≤ y and |y| ≤ |x|, then cosh′_{1} x − cosh′_{1} y = cosh′_{1}(x · y − \sqrt{(x^{2} − 1) · (y^{2} − 1)}).

(55) If 1 ≤ x and 1 ≤ y and |y| ≤ |x|, then cosh′_{2} x − cosh′_{2} y = cosh′_{2}(x · y − \sqrt{(x^{2} − 1) · (y^{2} − 1)}).

(56) If x^{2} < 1 and y^{2} < 1, then tanh′ x + tanh′ y = tanh′(\frac{x+y}{1+x·y}).

(57) If x^{2} < 1 and y^{2} < 1, then tanh′ x − tanh′ y = tanh′(\frac{x−y}{1−x·y}).

(58) If 0 < x and (\frac{x−1}{x+1})^{2} < 1, then log_{e} x = 2 · tanh′(\frac{x−1}{x+1}).

(59) If 0 < x and (\frac{x^{2}−1}{x^{2}+1})^{2} < 1, then log_{e} x = tanh′(\frac{x^{2}−1}{x^{2}+1}).

(60) If 1 < x and 1 ≤ \frac{x^{2}+1}{2·x}, then log_{e} x = cosh′_{1}(\frac{x^{2}+1}{2·x}).

(61) If 0 < x and x < 1 and 1 ≤ \frac{x^{2}+1}{2·x}, then log_{e} x = cosh′_{2}(\frac{x^{2}+1}{2·x}).

(62) If 0 < x, then log_{e} x = sinh′(\frac{x^{2}−1}{2·x}).

(63) If y = \frac{1}{2} · (exp x − exp(−x)), then x = log_{e}(y + \sqrt{y^{2} + 1}).

(64) If y = \frac{1}{2} · (exp x + exp(−x)) and 1 ≤ y, then x = log_{e}(y + \sqrt{y^{2} − 1}) or x = −log_{e}(y + \sqrt{y^{2} − 1}).

(65) If y = \frac{exp x−exp(−x)}{exp x+exp(−x)}, then x = \frac{1}{2} · log_{e}(\frac{1+y}{1−y}).

(66) If y = \frac{exp x+exp(−x)}{exp x−exp(−x)} and x ≠ 0, then x = \frac{1}{2} · log_{e}(\frac{y+1}{y−1}).

(67) If y = _{\frac{1}{\frac{exp x+exp(−x)}{2}}} , then x = log_{e}(^{\frac{1+\sqrt{1−y^{2}}}{y}}) or x = −log_{e}(^{\frac{1+\sqrt{1−y^{2}}}{y}}).

(68) If y = _{\frac{1}{\frac{exp x−exp(−x)}{2}}} and x ≠ 0, then x = log_{e}(^{\frac{1+\sqrt{1+y^{2}}}{y}}) or x =

log_{e}(^{\frac{1−\sqrt{1+y^{2}}}{y}}).

(69) (The function cosh)(2 · x) = 1 + 2 · (the function sinh)(x)^{2}.

(70) (The function cosh)(x)^{2} = 1 + (the function sinh)(x)^{2}.

(71) (The function sinh)(x)^{2} = (the function cosh)(x)^{2} − 1.

(72) sinh(5 · x) = 5 · sinh x + 20 · (sinh x)^{3} + 16 · (sinh x)^{5}.

formulas and identities of inverse … 387

(73) cosh(5 · x) = (5 · cosh x − 20 · (cosh x)^{3}) + 16 · (cosh x)^{5}.

References

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

[2] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 1990.

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

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

[5] Takashi Mitsuishi and Yuguang Yang. Properties of the trigonometric function. Formalized Mathematics, 8(1):103–106, 1999.

[6] Library Committee of the Association of Mizar Users. Binary operations on numbers. To appear in Formalized Mathematics.

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

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

[9] Yuguang Yang and Yasunari Shidama. Trigonometric functions and existence of circle ratio. Formalized Mathematics, 7(2):255–263, 1998.

388 fuguo ge and xiquan liang and yuzhong ding

Lines on Planes in n-Dimensional Euclidean Spaces

Akihiro Kubo Shinshu University, Nagano, Japan

Summary. In the paper we introduce basic properties of lines in the plane on this space. Lines and planes are expressed by the vector equation and are the image of ℝ and ℝ^{2}. By this, we can say that the properties of the classic Euclid geometry are satisfied also in R^{n} as we know them intuitively. Next, we define the metric between the point and the line of this space.

   MML identifier: EUCLIDLP, version: 7.5.01 4.39.921

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

We follow the rules: a, a_{1}, a_{2}, a_{3}, b, b_{1}, b_{2}, b_{3}, r, s, t, u are real numbers, n is a natural number, and x_{0}, x, x_{1}, x_{2}, x_{3}, y_{0}, y, y_{1}, y_{2}, y_{3} are elements of R^{n}.

One can prove the following propositions:

(1) \frac{s}{t} · (u · x) = \frac{s·u}{t} · x and \frac{1}{t} · (u · x) = \frac{u}{t} · x.

(2) x_{1} + (x_{2} + x_{3}) = (x_{1} + x_{2}) + x_{3}.

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

(4) ⟨\underbrace{0, …, 0}_{n}⟩ − x = −x.

(5) x_{1} − (x_{2} + x_{3}) = x_{1} − x_{2} − x_{3}.

(6) x_{1} − x_{2} = x_{1} + −x_{2}.

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

(8) −a · x = (−a) · x and −a · x = a · −x.

(9) x_{1} − (x_{2} − x_{3}) = (x_{1} − x_{2}) + x_{3}.

(10) x_{1} + (x_{2} − x_{3}) = (x_{1} + x_{2}) − x_{3}.

(11) x_{1} = x_{2} + x_{3} iff x_{2} = x_{1} − x_{3}.

(12) x = x_{1} + x_{2} + x_{3} iff x − x_{1} = x_{2} + x_{3}.

(13) −(x_{1} + x_{2} + x_{3}) = −x_{1} + −x_{2} + −x_{3}.

(14) x_{1} = x_{2} iff x_{1} − x_{2} = ⟨\underbrace{0, …, 0}_{n}⟩.

(15) If x_{1} − x_{0} = t · x and x_{1} ≠ x_{0}, then t ≠ 0.

(16) (a − b) · x = a · x + (−b) · x and (a − b) · x = a · x + −b · x and (a − b) · x = a · x − b · x.

(17) a · (x − y) = a · x + −a · y and a · (x − y) = a · x + (−a) · y and a · (x − y) = a · x − a · y.

(18) (s − t − u) · x = s · x − t · x − u · x.

(19) x − (a_{1} · x_{1} + a_{2} · x_{2} + a_{3} · x_{3}) = x + ((−a_{1}) · x_{1} + (−a_{2}) · x_{2} + (−a_{3}) · x_{3}).

(20) x − (s + t + u) · y = x + (−s) · y + (−t) · y + (−u) · y.

(21) (x_{1} + x_{2}) + (y_{1} + y_{2}) = x_{1} + y_{1} + (x_{2} + y_{2}).

(22) (x_{1} + x_{2} + x_{3}) + (y_{1} + y_{2} + y_{3}) = x_{1} + y_{1} + (x_{2} + y_{2}) + (x_{3} + y_{3}).

(23) (x_{1} + x_{2}) − (y_{1} + y_{2}) = (x_{1} − y_{1}) + (x_{2} − y_{2}).

(24) (x_{1} + x_{2} + x_{3}) − (y_{1} + y_{2} + y_{3}) = (x_{1} − y_{1}) + (x_{2} − y_{2}) + (x_{3} − y_{3}).

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

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

(27) a · (b_{1} · x_{1} + b_{2} · x_{2} + b_{3} · x_{3}) = a · b_{1} · x_{1} + a · b_{2} · x_{2} + a · b_{3} · x_{3}.

(28) a_{1} · x_{1} + a_{2} · x_{2} + (b_{1} · x_{1} + b_{2} · x_{2}) = (a_{1} + b_{1}) · x_{1} + (a_{2} + b_{2}) · x_{2}.

(29) a_{1} · x_{1} + a_{2} · x_{2} + a_{3} · x_{3} + (b_{1} · x_{1} + b_{2} · x_{2} + b_{3} · x_{3}) = ((a_{1} + b_{1}) · x_{1} + (a_{2} + b_{2}) · x_{2}) + (a_{3} + b_{3}) · x_{3}.

(30) (a_{1} · x_{1} + a_{2} · x_{2}) − (b_{1} · x_{1} + b_{2} · x_{2}) = (a_{1} − b_{1}) · x_{1} + (a_{2} − b_{2}) · x_{2}.

(31) (a_{1} · x_{1} + a_{2} · x_{2} + a_{3} · x_{3}) − (b_{1} · x_{1} + b_{2} · x_{2} + b_{3} · x_{3}) = (a_{1} − b_{1}) · x_{1} + (a_{2} − b_{2}) · x_{2} + (a_{3} − b_{3}) · x_{3}.

(32) If a_{1} + a_{2} + a_{3} = 1, then a_{1} · x_{1} + a_{2} · x_{2} + a_{3} · x_{3} = x_{1} + a_{2} · (x_{2} − x_{1}) + a_{3} · (x_{3} − x_{1}).

(33) If x = x_{1} + a_{2} · (x_{2} − x_{1}) + a_{3} · (x_{3} − x_{1}), then there exists a real number a_{1} such that x = a_{1} · x_{1} + a_{2} · x_{2} + a_{3} · x_{3} and a_{1} + a_{2} + a_{3} = 1.

(34) For every natural number n such that n ≥ 1 holds 1 ∗ n ≠ ⟨\underbrace{0, …, 0}_{n}⟩.

(35) For every subset A of R^{n} and for all x_{1}, x_{2} such that A is a line and x_{1} ∈ A and x_{2} ∈ A and x_{1} ≠ x_{2} holds A = Line(x_{1}, x_{2}).

(36) For all elements x_{1}, x_{2} of R^{n} such that y_{1} ∈ Line(x_{1}, x_{2}) and y_{2} ∈

Line(x_{1}, x_{2}) there exists a such that y_{2} − y_{1} = a · (x_{2} − x_{1}). Let us consider n and let x_{1}, x_{2} be elements of R^{n}. The predicate x_{1} ∥ x_{2}

is defined as follows:

lines on planes in n-dimensional … 391

(Def. 1) x_{1} ≠ ⟨\underbrace{0, …, 0}_{n}⟩ and x_{2} ≠ ⟨\underbrace{0, …, 0}_{n}⟩ and there exists r such that x_{1} = r·x_{2}.

One can prove the following proposition

(37) For all elements x_{1}, x_{2} of R^{n} such that x_{1} ∥ x_{2} there exists a such that a ≠ 0 and x_{1} = a · x_{2}.

Let us consider n and let x_{1}, x_{2} be elements of R^{n}. Let us note that the predicate x_{1} ∥ x_{2} is symmetric.

The following proposition is true

(38) If x_{1} ∥ x_{2} and x_{2} ∥ x_{3}, then x_{1} ∥ x_{3}.

Let n be a natural number and let x_{1}, x_{2} be elements of R^{n}. We say that x_{1} and x_{2} are linearly independent if and only if:

(Def. 2) For all real numbers a_{1}, a_{2} such that a_{1} · x_{1} + a_{2} · x_{2} = ⟨\underbrace{0, …, 0}_{n}⟩ holds

a_{1} = 0 and a_{2} = 0.

Let us note that the predicate x_{1} and x_{2} are linearly independent is symmetric.

Let us consider n and let x_{1}, x_{2} be elements of R^{n}. We introduce x_{1} and x_{2} are linearly dependent as an antonym of x_{1} and x_{2} are linearly independent.

Next we state a number of propositions:

(39) If x_{1} and x_{2} are linearly independent, then x_{1} ≠ ⟨\underbrace{0, …, 0}_{n}⟩ and x_{2} ≠

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

(40) For all x_{1}, x_{2} such that x_{1} and x_{2} are linearly independent holds if a_{1} · x_{1} + a_{2} · x_{2} = b_{1} · x_{1} + b_{2} · x_{2}, then a_{1} = b_{1} and a_{2} = b_{2}.

(41) Let given x_{1}, x_{2}, y_{1}, y_{1}. Suppose y_{1} and y_{2} are linearly independent. Suppose y_{1} = a_{1} ·x_{1} +a_{2} ·x_{2} and y_{2} = b_{1} ·x_{1} +b_{2} ·x_{2}. Then there exist real numbers c_{1}, c_{2}, d_{1}, d_{2} such that x_{1} = c_{1} ·y_{1} +c_{2} ·y_{2} and x_{2} = d_{1} ·y_{1} +d_{2} ·y_{2}.

(42) If x_{1} and x_{2} are linearly independent, then x_{1} ≠ x_{2}.

(43) If x_{2} − x_{1} and x_{3} − x_{1} are linearly independent, then x_{2} ≠ x_{3}.

(44) If x_{1} and x_{2} are linearly independent, then x_{1} + t · x_{2} and x_{2} are linearly independent.

(45) Suppose x_{1} − x_{0} and x_{3} − x_{2} are linearly independent and y_{0} ∈ Line(x_{0}, x_{1}) and y_{1} ∈ Line(x_{0}, x_{1}) and y_{0} ≠ y_{1} and y_{2} ∈ Line(x_{2}, x_{3}) and y_{3} ∈ Line(x_{2}, x_{3}) and y_{2} ≠ y_{3}. Then y_{1} − y_{0} and y_{3} − y_{2} are linearly independent.

(46) If x_{1} ∥ x_{2}, then x_{1} and x_{2} are linearly dependent and x_{1} ≠ ⟨\underbrace{0, …, 0}_{n}⟩

and x_{2} ≠ ⟨\underbrace{0, …, 0}_{n}⟩.

(47) If x_{1} and x_{2} are linearly dependent, then x_{1} = ⟨\underbrace{0, …, 0}_{n}⟩ or x_{2} =

⟨\underbrace{0, …, 0}_{n}⟩ or x_{1} ∥ x_{2}.

(48) For all elements x_{1}, x_{2}, y_{1} of R^{n} there exists an element y_{2} of R^{n} such

that y_{2} ∈ Line(x_{1}, x_{2}) and x_{1} − x_{2}, y_{1} − y_{2} are orthogonal. Let us consider n and let x_{1}, x_{2} be elements of R^{n}. The predicate x_{1} ⊥ x_{2}

is defined by: (Def. 3) x_{1} ≠ ⟨\underbrace{0, …, 0}_{n}⟩ and x_{2} ≠ ⟨\underbrace{0, …, 0}_{n}⟩ and x_{1}, x_{2} are orthogonal.

Let us note that the predicate x_{1} ⊥ x_{2} is symmetric.

The following propositions are true:

(49) If x ⊥ y_{0} and y_{0} ∥ y_{1}, then x ⊥ y_{1}.

(50) If x ⊥ y, then x and y are linearly independent.

(51) If x_{1} ∥ x_{2}, then x_{1} ⊥̸ x_{2}.

(52) If x_{1} ⊥ x_{2}, then x_{1} ∦ x_{2}.

Let us consider n. The functor Lines(R^{n}) yields a family of subsets of R^{n} and is defined by:

(Def. 4) Lines(R^{n}) = {Line(x_{1}, x_{2})}.

Let us consider n. Note that Lines(R^{n}) is non empty.

The following proposition is true

(53) Line(x_{1}, x_{2}) ∈ Lines(R^{n}).

In the sequel L, L_{0}, L_{1}, L_{2} are elements of Lines(R^{n}).

The following propositions are true:

(54) If x_{1} ∈ L and x_{2} ∈ L, then Line(x_{1}, x_{2}) ⊆ L.

(55) L_{1} meets L_{2} iff there exists x such that x ∈ L_{1} and x ∈ L_{2}.

(56) If L_{0} misses L_{1} and x ∈ L_{0}, then x ∉ L_{1}.

(57) There exist x_{1}, x_{2} such that L = Line(x_{1}, x_{2}).

(58) There exists x such that x ∈ L.

(59) If x_{0} ∈ L and L is a line, then there exists x_{1} such that x_{1} ≠ x_{0} and x_{1} ∈ L.

(60) If x ∉ L and L is a line, then there exist x_{1}, x_{2} such that L = Line(x_{1}, x_{2}) and x − x_{1} ⊥ x_{2} − x_{1}.

(61) If x ∉ L and L is a line, then there exist x_{1}, x_{2} such that L = Line(x_{1}, x_{2})

and x − x_{1} and x_{2} − x_{1} are linearly independent. Let n be a natural number, let x be an element of R^{n}, and let L be an

element of Lines(R^{n}). The functor ρ(x, L) yields a real number and is defined by:

(Def. 5) There exists a subset S of ℝ such that S = {|x − x_{0}|; x_{0} ranges over

elements of R^{n}: x_{0} ∈ L} and ρ(x, L) = inf S. Next we state three propositions:

(62) There exists x_{0} such that x_{0} ∈ L and |x − x_{0}| = ρ(x, L).

(63) ρ(x, L) ≥ 0.

(64) x ∈ L iff ρ(x, L) = 0.

Let us consider n and let us consider L_{1}, L_{2}. The predicate L_{1} ∥ L_{2} is defined as follows:

(Def. 6) There exist elements x_{1}, x_{2}, y_{1}, y_{2} of R^{n} such that L_{1} = Line(x_{1}, x_{2})

and L_{2} = Line(y_{1}, y_{2}) and x_{2} − x_{1} ∥ y_{2} − y_{1}. Let us note that the predicate L_{1} ∥ L_{2} is symmetric.

The following proposition is true

(65) If L_{0} ∥ L_{1} and L_{1} ∥ L_{2}, then L_{0} ∥ L_{2}.

Let us consider n and let us consider L_{1}, L_{2}. The predicate L_{1} ⊥ L_{2} is defined by:

(Def. 7) There exist elements x_{1}, x_{2}, y_{1}, y_{2} of R^{n} such that L_{1} = Line(x_{1}, x_{2})

and L_{2} = Line(y_{1}, y_{2}) and x_{2} − x_{1} ⊥ y_{2} − y_{1}. Let us note that the predicate L_{1} ⊥ L_{2} is symmetric.

We now state a number of propositions:

(66) If L_{0} ⊥ L_{1} and L_{1} ∥ L_{2}, then L_{0} ⊥ L_{2}.

(67) If x ∉ L and L is a line, then there exists L_{0} such that x ∈ L_{0} and L_{0} ⊥ L and L_{0} meets L.

(68) If L_{1} misses L_{2}, then there exists x such that x ∈ L_{1} and x ∉ L_{2}.

(69) If x_{1} ∈ L and x_{2} ∈ L and x_{1} ≠ x_{2}, then Line(x_{1}, x_{2}) = L and L is a line.

(70) If L_{1} is a line and L_{2} is a line and L_{1} = L_{2}, then L_{1} ∥ L_{2}.

(71) If L_{1} ∥ L_{2}, then L_{1} is a line and L_{2} is a line.

(72) If L_{1} ⊥ L_{2}, then L_{1} is a line and L_{2} is a line.

(73) If x ∈ L and a ≠ 1 and a · x ∈ L, then ⟨\underbrace{0, …, 0}_{n}⟩ ∈ L.

(74) If x_{1} ∈ L and x_{2} ∈ L, then there exists x_{3} such that x_{3} ∈ L and x_{3} − x_{1} = a · (x_{2} − x_{1}).

(75) If x_{1} ∈ L and x_{2} ∈ L and x_{3} ∈ L and x_{1} ≠ x_{2}, then there exists a such that x_{3} − x_{1} = a · (x_{2} − x_{1}).

(76) If L_{1} ∥ L_{2} and L_{1} ≠ L_{2}, then L_{1} misses L_{2}.

(77) If L_{1} ∥ L_{2}, then L_{1} = L_{2} or L_{1} misses L_{2}.

(78) If L_{1} ∥ L_{2} and L_{1} meets L_{2}, then L_{1} = L_{2}.

(79) If L is a line, then there exists L_{0} such that x ∈ L_{0} and L_{0} ∥ L.

(80) For all x, L such that x ∉ L and L is a line there exists L_{0} such that x ∈ L_{0} and L_{0} ∥ L and L_{0} ≠ L.

(81) For all x_{0}, x_{1}, y_{0}, y_{1}, L_{1}, L_{2} such that x_{0} ∈ L_{1} and x_{1} ∈ L_{1} and x_{0} ≠ x_{1} and y_{0} ∈ L_{2} and y_{1} ∈ L_{2} and y_{0} ≠ y_{1} and L_{1} ⊥ L_{2} holds x_{1} −x_{0} ⊥ y_{1} −y_{0}.

(82) For all L_{1}, L_{2} such that L_{1} ⊥ L_{2} holds L_{1} ≠ L_{2}.

(83) For all x_{1}, x_{2}, L such that L is a line and L = Line(x_{1}, x_{2}) holds x_{1} ≠ x_{2}.

(84) If x_{0} ∈ L_{1} and x_{1} ∈ L_{1} and x_{0} ≠ x_{1} and y_{0} ∈ L_{2} and y_{1} ∈ L_{2} and y_{0} ≠ y_{1} and L_{1} ∥ L_{2}, then x_{1} − x_{0} ∥ y_{1} − y_{0}.

(85) Suppose x_{2} − x_{1} and x_{3} − x_{1} are linearly independent and y_{2} ∈ Line(x_{1}, x_{2}) and y_{3} ∈ Line(x_{1}, x_{3}) and L_{1} = Line(x_{2}, x_{3}) and L_{2} = Line(y_{2}, y_{3}). Then L_{1} ∥ L_{2} if and only if there exists a such that a ≠ 0 and y_{2} − x_{1} = a · (x_{2} − x_{1}) and y_{3} − x_{1} = a · (x_{3} − x_{1}).

(86) For all L_{1}, L_{2} such that L_{1} is a line and L_{2} is a line and L_{1} ≠ L_{2} there exists x such that x ∈ L_{1} and x ∉ L_{2}.

(87) For all x, L_{1}, L_{2} such that L_{1} ⊥ L_{2} and x ∈ L_{2} there exists L_{0} such that x ∈ L_{0} and L_{0} ⊥ L_{2} and L_{0} ∥ L_{1}.

(88) For all x, L_{1}, L_{2} such that x ∈ L_{1} and x ∈ L_{2} and L_{1} ⊥ L_{2} there exists x_{0} such that x ≠ x_{0} and x_{0} ∈ L_{1} and x_{0} ∉ L_{2}.

Let n be a natural number and let x_{1}, x_{2}, x_{3} be elements of R^{n}. The functor Plane(x_{1}, x_{2}, x_{3}) yielding a subset of R^{n} is defined as follows:

(Def. 8) Plane(x_{1}, x_{2}, x_{3}) = {a_{1} · x_{1} + a_{2} · x_{2} + a_{3} · x_{3} : a_{1} + a_{2} + a_{3} = 1}.

Let n be a natural number and let x_{1}, x_{2}, x_{3} be elements of R^{n}. One can check that Plane(x_{1}, x_{2}, x_{3}) is non empty.

Let us consider n and let A be a subset of R^{n}. We say that A is plane if and only if:

(Def. 9) There exist x_{1}, x_{2}, x_{3} such that x_{2} − x_{1} and x_{3} − x_{1} are linearly inde-

pendent and A = Plane(x_{1}, x_{2}, x_{3}). One can prove the following propositions:

(89) x_{1} ∈ Plane(x_{1}, x_{2}, x_{3}) and x_{2} ∈ Plane(x_{1}, x_{2}, x_{3}) and x_{3} ∈ Plane(x_{1}, x_{2}, x_{3}).

(90) If x_{1} ∈ Plane(y_{1}, y_{2}, y_{3}) and x_{2} ∈ Plane(y_{1}, y_{2}, y_{3}) and x_{3} ∈ Plane(y_{1}, y_{2}, y_{3}), then Plane(x_{1}, x_{2}, x_{3}) ⊆ Plane(y_{1}, y_{2}, y_{3}).

(91) Let A be a subset of R^{n} and given x, x_{1}, x_{2}, x_{3}. Suppose x ∈ Plane(x_{1}, x_{2}, x_{3}) and there exist real numbers c_{1}, c_{2}, c_{3} such that c_{1} +c_{2} +

c_{3} = 0 and x = c_{1} · x_{1} + c_{2} · x_{2} + c_{3} · x_{3}. Then ⟨\underbrace{0, …, 0}_{n}⟩ ∈ Plane(x_{1}, x_{2}, x_{3}).

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

(93) For every subset A of R^{n} and for every x such that A is plane and x ∈ A and there exists a such that a ≠ 1 and a · x ∈ A holds ⟨\underbrace{0, …, 0}_{n}⟩ ∈ A.

(94) If x_{1} − x_{1} and x_{3} − x_{1} are linearly independent and x ∈ Plane(x_{1}, x_{2}, x_{3})

and x = a_{1} · x_{1} + a_{2} · x_{2} + a_{3} · x_{3}, then a_{1} + a_{2} + a_{3} = 1 or ⟨\underbrace{0, …, 0}_{n}⟩ ∈

Plane(x_{1}, x_{2}, x_{3}).

(95) x ∈ Plane(x_{1}, x_{2}, x_{3}) iff there exist a_{1}, a_{2}, a_{3} such that a_{1} + a_{2} + a_{3} = 1 and x = a_{1} · x_{1} + a_{2} · x_{2} + a_{3} · x_{3}.

(96) Suppose that (i) x_{2} − x_{1} and x_{3} − x_{1} are linearly independent, (ii) x ∈ Plane(x_{1}, x_{2}, x_{3}), (iii) a_{1} + a_{2} + a_{3} = 1, (iv) x = a_{1} · x_{1} + a_{2} · x_{2} + a_{3} · x_{3},

(v) b_{1} + b_{2} + b_{3} = 1, and (vi) x = b_{1} · x_{1} + b_{2} · x_{2} + b_{3} · x_{3}.

Then a_{1} = b_{1} and a_{2} = b_{2} and a_{3} = b_{3}. Let us consider n. The functor Planes(R^{n}) yielding a family of subsets of

R^{n} is defined by: (Def. 10) Planes(R^{n}) = {Plane(x_{1}, x_{2}, x_{3})}.

Let us consider n. Note that Planes(R^{n}) is non empty.

The following proposition is true

(97) Plane(x_{1}, x_{2}, x_{3}) ∈ Planes(R^{n}).

In the sequel P, P_{0}, P_{1}, P_{2} are elements of Planes(R^{n}).

Next we state several propositions:

(98) If x_{1} ∈ P and x_{2} ∈ P and x_{3} ∈ P, then Plane(x_{1}, x_{2}, x_{3}) ⊆ P.

(99) If x_{1} ∈ P and x_{2} ∈ P and x_{3} ∈ P and x_{2} − x_{1} and x_{3} − x_{1} are linearly independent, then P = Plane(x_{1}, x_{2}, x_{3}).

(100) If P_{1} is plane and P_{1} ⊆ P_{2}, then P_{1} = P_{2}.

(101) Line(x_{1}, x_{2}) ⊆ Plane(x_{1}, x_{2}, x_{3}) and Line(x_{2}, x_{3}) ⊆ Plane(x_{1}, x_{2}, x_{3}) and Line(x_{3}, x_{1}) ⊆ Plane(x_{1}, x_{2}, x_{3}).

(102) If x_{1} ∈ P and x_{2} ∈ P, then Line(x_{1}, x_{2}) ⊆ P.

Let n be a natural number and let L_{1}, L_{2} be elements of Lines(R^{n}). We say that L_{1} and L_{2} are coplanar if and only if:

(Def. 11) There exist elements x_{1}, x_{2}, x_{3} of R^{n} such that L_{1} ⊆ Plane(x_{1}, x_{2}, x_{3})

and L_{2} ⊆ Plane(x_{1}, x_{2}, x_{3}). We now state a number of propositions:

(103) L_{1} and L_{2} are coplanar iff there exists P such that L_{1} ⊆ P and L_{2} ⊆ P.

(104) If L_{1} ∥ L_{2}, then L_{1} and L_{2} are coplanar.

(105) Suppose L_{1} is a line and L_{2} is a line and L_{1} and L_{2} are coplanar and L_{1} misses L_{2}. Then there exists P such that L_{1} ⊆ P and L_{2} ⊆ P and P is plane.

(106) There exists P such that x ∈ P and L ⊆ P.

(107) If x ∉ L and L is a line, then there exists P such that x ∈ P and L ⊆ P and P is plane.

(108) If x ∈ P and L ⊆ P and x ∉ L and L is a line, then P is plane.

(109) If x ∉ L and L is a line and x ∈ P_{0} and L ⊆ P_{0} and x ∈ P_{1} and L ⊆ P_{1}, then P_{0} = P_{1}.

(110) If L_{1} is a line and L_{2} is a line and L_{1} and L_{2} are coplanar and L_{1} ≠ L_{2}, then there exists P such that L_{1} ⊆ P and L_{2} ⊆ P and P is plane.

(111) For all L_{1}, L_{2} such that L_{1} is a line and L_{2} is a line and L_{1} ≠ L_{2} and L_{1} meets L_{2} there exists P such that L_{1} ⊆ P and L_{2} ⊆ P and P is plane.

(112) If L_{1} is a line and L_{2} is a line and L_{1} ≠ L_{2} and L_{1} meets L_{2} and L_{1} ⊆ P_{1} and L_{2} ⊆ P_{1} and L_{1} ⊆ P_{2} and L_{2} ⊆ P_{2}, then P_{1} = P_{2}.

(113) If L_{1} ∥ L_{2} and L_{1} ≠ L_{2}, then there exists P such that L_{1} ⊆ P and L_{2} ⊆ P and P is plane.

(114) If L_{1} ⊥ L_{2} and L_{1} meets L_{2}, then there exists P such that P is plane and L_{1} ⊆ P and L_{2} ⊆ P.

(115) If L_{0} ⊆ P and L_{1} ⊆ P and L_{2} ⊆ P and x ∈ L_{0} and x ∈ L_{1} and x ∈ L_{2} and L_{0} ⊥ L_{2} and L_{1} ⊥ L_{2}, then L_{0} = L_{1}.

(116) If L_{1} and L_{2} are coplanar and L_{1} ⊥ L_{2}, then L_{1} meets L_{2}.

(117) If L_{1} ⊆ P and L_{2} ⊆ P and L_{1} ⊥ L_{2} and x ∈ P and L_{0} ∥ L_{2} and x ∈ L_{0}, then L_{0} ⊆ P and L_{0} ⊥ L_{1}.

(118) If L ⊆ P and L_{1} ⊆ P and L_{2} ⊆ P and L ⊥ L_{1} and L ⊥ L_{2}, then L_{1} ∥ L_{2}.

(119) Suppose L_{0} ⊆ P and L_{1} ⊆ P and L_{2} ⊆ P and L_{0} ∥ L_{1} and L_{1} ∥ L_{2} and L_{0} ≠ L_{1} and L_{1} ≠ L_{2} and L_{2} ≠ L_{0} and L meets L_{0} and L meets L_{1}. Then L meets L_{2}.

(120) If L_{1} and L_{2} are coplanar and L_{1} is a line and L_{2} is a line and L_{1} misses L_{2}, then L_{1} ∥ L_{2}.

(121) If x_{1} ∈ P and x_{2} ∈ P and y_{1} ∈ P and y_{2} ∈ P and x_{2} − x_{1} and y_{2} − y_{1} are linearly independent, then Line(x_{1}, x_{2}) meets Line(y_{1}, y_{2}).

References

[1] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 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. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.

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

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

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

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

[10] Akihiro Kubo. Lines in n-dimensional Euclidean spaces. Formalized Mathematics, 11(4):371–376, 2003.

[11] Yatsuka Nakamura, Andrzej Trybulec, and Czesław Byliński. Bounded domains and unbounded domains. Formalized Mathematics, 8(1):1–13, 1999.

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

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

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

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

398 akihiro kubo

Cardinal Numbers and Finite Sets^{1}

Karol Pa̧k Institute of Mathematics University of Białystok Akademicka 2, 15-267 Białystok, Poland

Summary. In this paper we define class of functions and operators needed for the proof of the principle of inclusions and the disconnections. We also given certain cardinal numbers concerning elementary class of functions (this function mapping finite set in finite set).

MML identifier: CARD FIN, version: 7.5.01 4.39.921

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

For simplicity, we use the following convention: x, x_{1}, x_{2}, y, z, X′ denote sets, X, Y denote finite sets, n, k, m denote natural numbers, and f denotes a function.

Next we state the proposition

(1) If X ⊆ Y and card X = card Y, then X = Y. In the sequel F is a function from X ∪ {x} into Y ∪ {y}. One can prove the following proposition

(2) For all X, Y, x, y such that if Y = ∅, then X = ∅ and x ∉ X holds card(Y^{X}) = \overline{\overline{\{F : rng(F ↾X) ⊆ Y ∧ F (x) = y\}}}.

In the sequel F is a function from X ∪ {x} into Y. One can prove the following two propositions:

(3) For all X, Y, x, y such that x ∉ X and y ∈ Y holds card(Y^{X}) = \overline{\overline{\{F : F (x) = y\}}}.

1This work has been partially supported by the KBN grant 4 T11C 039 24 and the FP6 IST grant TYPES No. 510096.

(4) If if Y = ∅, then X = ∅, then card(Y^{X}) = (card Y)^{card X}. In the sequel F_{1} denotes a function from X into Y and F_{2} denotes a function

from X ∪ {x} into Y ∪ {y}.

One can prove the following two propositions:

(5) Let given X, Y, x, y. Suppose if Y is empty, then X is empty and x ∉ X and y ∉ Y. Then \overline{\overline{\{F_{1} : F_{1} is one-to-one\}}} = \overline{\overline{\{F_{2} : F_{2} is one-to-one ∧ F_{2}(x) = y\}}}.

(6) \frac{n!}{(n−′k)!} is a natural number. In the sequel F is a function from X into Y. The following proposition is true

(7) If card X ≤ card Y, then \overline{\overline{\{F : F is one-to-one\}}} = \frac{(card Y)!}{(card Y −′card X)!}. In the sequel F denotes a function from X into X. The following proposition is true

(8) \overline{\overline{\{F : F is a permutation of X\}}} = (card X)!. Let us consider X, k, x_{1}, x_{2}. The functor Choose(X, k, x_{1}, x_{2}) yields a subset

of {x_{1}, x_{2}}^{X} and is defined as follows: (Def. 1) x ∈ Choose(X, k, x_{1}, x_{2}) iff there exists a function f from X into {x_{1}, x_{2}}

such that f = x and \overline{\overline{f^{−1}(\{x_{1}\})}} = k. We now state several propositions:

(9) If card X ≠ k, then Choose(X, k, x_{1}, x_{1}) is empty.

(10) If card X < k, then Choose(X, k, x_{1}, x_{2}) is empty.

(11) If x_{1} ≠ x_{2}, then card Choose(X, 0, x_{1}, x_{2}) = 1.

(12) card Choose(X, card X, x_{1}, x_{2}) = 1.

(13) If f(y) = x and y ∈ dom f, then {y} ∪ (f↾(dom f \ {y}))^{−1}({x}) =

f^{−1}({x}). In the sequel g denotes a function from X ∪ {z} into {x, y}. The following propositions are true:

(14) If z ∉ X, then card Choose(X, k, x, y) = \overline{\overline{\{g : \overline{\overline{g^{−1}(\{x\})}} = k + 1 ∧ g(z) = x\}}}.

(15) If f(y) ≠ x, then (f↾(dom f \ {y}))^{−1}({x}) = f^{−1}({x}).

(16) If z ∉ X and x ≠ y, then card Choose(X, k, x, y) = \overline{\overline{\{g : \overline{\overline{g^{−1}(\{x\})}} = k ∧ g(z) = y\}}}.

(17) If x ≠ y and z ∉ X, then card Choose(X ∪ {z}, k + 1, x, y) = card Choose(X, k + 1, x, y) + card Choose(X, k, x, y).

(18) If x ≠ y, then card Choose(X, k, x, y) = \binom{card X}{k}.

(19) If x ≠ y, then (Y ⟼ y)+·(X ⟼ x) ∈ Choose(X ∪ Y, card X, x, y).

(20) If x ≠ y and X misses Y, then (X ⟼ x)+·(Y ⟼ y) ∈ Choose(X ∪

Y, card X, x, y). Let F, C_{1} be functions and let y be a set. The functor Intersection(F, C_{1}, y)

yielding a subset of ⋃ rng F is defined as follows: (Def. 2) z ∈ Intersection(F, C_{1}, y) iff z ∈ ⋃ rng F and for every x such that

x ∈ dom C_{1} and C_{1}(x) = y holds z ∈ F (x). In the sequel F, C_{1} denote functions. The following propositions are true:

(21) For all F, C_{1} such that dom F ∩ C_{1}^{−1}({x}) is non empty holds y ∈ Intersection(F, C_{1}, x) iff for every z such that z ∈ dom C_{1} and C_{1}(z) = x holds y ∈ F (z).

(22) If Intersection(F, C_{1}, y) is non empty, then C_{1}^{−1}({y}) ⊆ dom F.

(23) If Intersection(F, C_{1}, y) is non empty, then for all x_{1}, x_{2} such that x_{1} ∈ C_{1}^{−1}({y}) and x_{2} ∈ C_{1}^{−1}({y}) holds F (x_{1}) meets F (x_{2}).

(24) If z ∈ Intersection(F, C_{1}, y) and y ∈ rng C_{1}, then there exists x such that x ∈ dom C_{1} and C_{1}(x) = y and z ∈ F (x).

(25) If F is empty or ⋃ rng F is empty, then Intersection(F, C_{1}, y) = ⋃ rng F.

(26) If F ↾C_{1}^{−1}({y}) = C_{1}^{−1}({y}) ⟼ ⋃ rng F, then Intersection(F, C_{1}, y) = ⋃ rng F.

(27) If ⋃ rng F is non empty and Intersection(F, C_{1}, y) = ⋃ rng F, then F ↾C_{1}^{−1}({y}) = C_{1}^{−1}({y}) ⟼ ⋃ rng F.

(28) Intersection(F, ∅, y) = ⋃ rng F.

(29) Intersection(F, C_{1}, y) ⊆ Intersection(F, C_{1}↾X′, y).

(30) If C_{1}^{−1}({y}) = (C_{1}↾X′)^{−1}({y}), then Intersection(F, C_{1}, y) = Intersection(F, C_{1}↾X′, y).

(31) Intersection(F ↾X′, C_{1}, y) ⊆ Intersection(F, C_{1}, y).

(32) If y ∈ rng C_{1} and C_{1}^{−1}({y}) ⊆ X′, then Intersection(F ↾X′, C_{1}, y) = Intersection(F, C_{1}, y).

(33) If x ∈ C_{1}^{−1}({y}), then Intersection(F, C_{1}, y) ⊆ F (x).

(34) If x ∈ C_{1}^{−1}({y}), then Intersection(F, C_{1}↾(dom C_{1} \ {x}), y) ∩ F (x) = Intersection(F, C_{1}, y).

(35) For all functions C_{2}, C_{3} such that C_{2}^{−1}({x_{1}}) = C_{3}^{−1}({x_{2}}) holds Intersection(F, C_{2}, x_{1}) = Intersection(F, C_{3}, x_{2}).

(36) If C_{1}^{−1}({y}) = ∅, then Intersection(F, C_{1}, y) = ⋃ rng F.

(37) If {x} = C_{1}^{−1}({y}), then Intersection(F, C_{1}, y) = F (x).

(38) If {x_{1}, x_{2}} = C_{1}^{−1}({y}), then Intersection(F, C_{1}, y) = F (x_{1}) ∩ F (x_{2}).

(39) For every F such that F is non empty holds y ∈ Intersection(F, dom F ⟼ x, x) iff for every z such that z ∈ dom F holds y ∈ F (z).

Let F be a function. We say that F is finite-yielding if and only if: (Def. 3) For every x holds F (x) is finite.

Let us observe that there exists a function which is non empty and finiteyielding and there exists a function which is empty and finite-yielding.

Let F be a finite-yielding function and let x be a set. Observe that F (x) is finite.

Let F be a finite-yielding function and let X be a set. One can check that F ↾X is finite-yielding.

Let F be a finite-yielding function and let G be a function. Note that F · G is finite-yielding and Intersect(F, G) is finite-yielding.

In the sequel F_{3} is a finite-yielding function. The following two propositions are true:

(40) If y ∈ rng C_{1}, then Intersection(F_{3}, C_{1}, y) is finite.

(41) If dom F_{3} is finite, then ⋃ rng F_{3} is finite.

Let F be a finite 0-sequence and let us consider n. Then F ↾n is a finite 0-sequence.

Let D be a set, let F be a finite 0-sequence of D, and let us consider n. Then F ↾n is a finite 0-sequence of D.

In the sequel D is a non empty set and b is a binary operation on D. Next we state several propositions:

(42) For every finite 0-sequence F of D and for all b, n such that n ∈ dom F but b has a unity or n ≠ 0 holds b(b ⊙ F ↾n, F (n)) = b ⊙ F ↾(n + 1).

(43) For every finite 0-sequence F of D and for every n such that len F = n+1 holds F = (F ↾n)^{⌢} ⟨F (n)⟩.

(44) For every finite 0-sequence F of ℕ and for every n such that n ∈ dom F holds ∑(F ↾n) + F (n) = ∑(F ↾(n + 1)).

(45) For every finite 0-sequence F of ℕ and for every n such that rng F ⊆ {0, n} holds ∑ F = n · card(F^{−1}({n})).

(46) x ∈ Choose(n, k, 1, 0) iff there exists a finite 0-sequence F of ℕ such that F = x and dom F = n and rng F ⊆ {0, 1} and ∑ F = k.

(47) For every finite 0-sequence F of D and for every b such that b has a unity or len F ≥ 1 holds b ⊙ F = b ⊙ XFS2FS(F).

(48) Let F, G be finite 0-sequences of D and P be a permutation of dom F. Suppose b is commutative and associative but b has a unity or len F ≥ 1 but G = F · P. Then b ⊙ F = b ⊙ G.

Let us consider k and let F be a finite-yielding function. Let us assume that dom F is finite. The card intersection of F wrt k yielding a natural number is defined by the condition (Def. 4).

(Def. 4) Let x, y be sets, X be a finite set, and P be a function from card Choose(X, k, x, y) into Choose(X, k, x, y). Suppose dom F = X and P is one-to-one and x ≠ y. Then there exists a finite 0-sequence X_{1} of ℕ such that dom X_{1} = dom P and for all z, f such that z ∈ dom X_{1} and f = P (z) holds X_{1}(z) = \overline{\overline{Intersection(F, f, x)}} and the card intersection of F wrt k = ∑ X_{1}.

One can prove the following propositions:

(49) Let x, y be sets, X be a finite set, and P be a function from card Choose(X, k, x, y) into Choose(X, k, x, y). Suppose dom F_{3} = X and P is one-to-one and x ≠ y. Let X_{1} be a finite 0-sequence of ℕ. Suppose dom X_{1} = dom P and for all z, f such that z ∈ dom X_{1} and f = P (z) holds X_{1}(z) = \overline{\overline{Intersection(F_{3}, f, x)}}. Then the card intersection of F_{3} wrt k = ∑ X_{1}.

(50) If dom F_{3} is finite and k = 0, then the card intersection of F_{3} wrt k = \overline{\overline{⋃ rng F_{3}}} .

(51) If dom F_{3} = X and k > card X, then the card intersection of F_{3} wrt k = 0.

(52) Let given F_{3}, X. Suppose dom F_{3} = X. Let P be a function from card X into X. Suppose P is one-to-one. Then there exists a finite 0sequence X_{1} of ℕ such that dom X_{1} = card X and for every z such that z ∈ dom X_{1} holds X_{1}(z) = card(F_{3} · P)(z) and the card intersection of F_{3} wrt 1 = ∑ X_{1}.

(53) If dom F_{3} = X, then the card intersection of F_{3} wrt card X = \overline{\overline{Intersection(F_{3}, X ⟼ x, x)}}.

(54) If F_{3} = {x} ⟼ X, then the card intersection of F_{3} wrt 1 = card X.

(55) Suppose x ≠ y and F_{3} = [x ⟼ X, y ⟼ Y]. Then the card intersection of F_{3} wrt 1 = card X + card Y and the card intersection of F_{3} wrt 2 = card(X ∩ Y).

(56) Let given F_{3}, x. Suppose dom F_{3} is finite and x ∈ dom F_{3}. Then the card intersection of F_{3} wrt 1 = (the card intersection of F_{3}↾(dom F_{3} \ {x}) wrt 1)+ card F_{3}(x).

(57) dom Intersect(F, dom F ⟼ X′) = dom F and for every x such that x ∈ dom F holds (Intersect(F, dom F ⟼ X′))(x) = F (x) ∩ X′.

(58) ⋃ rng F ∩ X′ = ⋃ rng Intersect(F, dom F ⟼ X′).

(59) Intersection(F, C_{1}, y) ∩ X′ = Intersection(Intersect(F, dom F ⟼ X′), C_{1}, y).

(60) Let F, G be finite 0-sequences. Suppose F is one-to-one and G is oneto-one and rng F misses rng G. Then F ^{⌢} G is one-to-one.

(61) Let given F_{3}, X, x, n. Suppose dom F_{3} = X and x ∈ dom F_{3} and k > 0. Then the card intersection of F_{3} wrt k + 1 = (the card intersection of F_{3}↾(dom F_{3} \ {x}) wrt k + 1) + (the card intersection of

Intersect(F_{3}↾(dom F_{3} \ {x}), dom F_{3} \ {x} ⟼ F_{3}(x)) wrt k).

(62) Let F, G, b_{1} be finite 0-sequences of D. Suppose that (i) b is commutative and associative, (ii) b has a unity or len F ≥ 1, (iii) len F = len G, (iv) len F = len b_{1}, and

(v) for every n such that n ∈ dom b_{1} holds b_{1}(n) = b(F (n), G(n)). Then b ⊙ F ^{⌢} G = b ⊙ b_{1}.

Let F_{4} be a finite 0-sequence of ℤ. The functor ∑ F_{4} yielding an integer is defined as follows:

(Def. 5) ∑ F_{4} = +_{ℤ} ⊙ F_{4}.

Let F_{4} be a finite 0-sequence of ℤ and let us consider x. Then F_{4}(x) is an integer.

Next we state several propositions:

(63) For every finite 0-sequence F_{5} of ℕ and for every finite 0-sequence F_{4} of ℤ such that F_{4} = F_{5} holds ∑ F_{4} = ∑ F_{5}.

(64) Let F, F_{4} be finite 0-sequences of ℤ and i be an integer. If dom F = dom F_{4} and for every n such that n ∈ dom F holds i · F (n) = F_{4}(n), then i · ∑ F = ∑ F_{4}.

(65) If x ∈ dom F, then ⋃ rng F = ⋃ rng(F ↾(dom F \ {x})) ∪ F (x).

(66) Let F_{3} be a finite-yielding function and given X. Then there exists a finite 0-sequence X_{1} of ℤ such that dom X_{1} = card X and for every n such that n ∈ dom X_{1} holds X_{1}(n) = (−1)^{n} · the card intersection of F_{3} wrt n + 1.

(67) Let F_{3} be a finite-yielding function and given X. Suppose dom F_{3} = X. Let X_{1} be a finite 0-sequence of ℤ. Suppose dom X_{1} = card X and for every n such that n ∈ dom X_{1} holds X_{1}(n) = (−1)^{n} · the card intersection of F_{3} wrt n + 1. Then \overline{\overline{⋃ rng F_{3}}} = ∑ X_{1}.

(68) Let given F_{3}, X, n, k. Suppose dom F_{3} = X. Given x, y such that x ≠ y and for every f such that f ∈ Choose(X, k, x, y) holds \overline{\overline{Intersection(F_{3}, f, x)}} = n. Then the card intersection of F_{3} wrt k = n · \binom{card X}{k}.

(69) Let given F_{3}, X. Suppose dom F_{3} = X. Let X_{2} be a finite 0-sequence of ℕ. Suppose dom X_{2} = card X and for every n such that n ∈ dom X_{2} there exist x, y such that x ≠ y and for every f such that f ∈ Choose(X, n + 1, x, y) holds \overline{\overline{Intersection(F_{3}, f, x)}} = X_{2}(n). Then there exists a finite 0sequence F of ℤ such that dom F = card X and \overline{\overline{⋃ rng F_{3}}} = ∑ F and for every n such that n ∈ dom F holds F (n) = (−1)^{n} · X_{2}(n) · \binom{card X}{n+1}.

In the sequel g denotes a function from X into Y.

The following propositions are true:

(70) Let X, Y be finite sets. Suppose X is non empty and Y is non empty. Then there exists a finite 0-sequence F of ℤ such that dom F = card Y +1 and ∑ F = \overline{\overline{\{g : g is onto\}}} and for every n such that n ∈ dom F holds F (n) = (−1)^{n} · \binom{card Y}{n} · (card Y − n)^{card X}.

(71) Let given n, k. Suppose k ≤ n. Then there exists a finite 0-sequence F of ℤ such that n block k = \frac{1}{k!} · ∑ F and dom F = k + 1 and for every m such that m ∈ dom F holds F (m) = (−1)^{m} · \binom{k}{m} · (k − m)^{n}.

In the sequel A, B are finite sets and f is a function from A into B. One can prove the following proposition

(72) Let given A, B and X be a finite set. Suppose if B is empty, then A is empty and X ⊆ A. Let F be a function from A into B. Suppose F is one-to-one and card A = card B. Then (card A −′ card X)! = {f : f is one-to-one ∧ rng(f↾(A \ X)) ⊆ F^{∘}(A \ X) ∧ \overline{\overline{⋀_{x} (x ∈ X ⇒ f(x) = F (x))\}}}.

In the sequel F denotes a function and h denotes a function from X into rng F.

The following proposition is true

(73) Let given F. Suppose dom F = X and F is one-to-one. Then there

exists a finite 0-sequence X_{2} of ℤ such that

(i) ∑ X_{2} = \overline{\overline{\{h : h is one-to-one ∧ ⋀_{x} (x ∈ X ⇒ h(x) ≠ F (x))\}}}, (ii) dom X_{2} = card X + 1, and (iii) for every n such that n ∈ dom X_{2} holds X_{2}(n) = \frac{(−1)^{n}·(card X)!}{n!}. In the sequel h is a function from X into X. The following proposition is true

(74) There exists a finite 0-sequence X_{2} of ℤ such that (i) ∑ X_{2} = \overline{\overline{\{h : h is one-to-one ∧ ⋀_{x} (x ∈ X ⇒ h(x) ≠ x)\}}}, (ii) dom X_{2} = card X + 1, and (iii) for every n such that n ∈ dom X_{2} holds X_{2}(n) = \frac{(−1)^{n}·(card X)!}{n!}.

References

290, 1990. 9(4):745–754, 2001. sequences. Formalized Mathematics, 1(1):107–114, 1990. 65, 1990.

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

[2] Grzegorz Bancerek. Sequences of ordinal numbers. Formalized Mathematics, 1(2):281– [3] Grzegorz Bancerek. Miscellaneous facts about functors. Formalized Mathematics, [4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite [5] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

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

406 karol pa̧k

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

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

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

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

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

[13] Takaya Nishiyama, Hirofumi Fukura, and Yatsuka Nakamura. Logical correctness of vector calculation programs. Formalized Mathematics, 12(3):375–380, 2004.

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

[15] Library Committee of the Association of Mizar Users. Binary operations on numbers. To appear in Formalized Mathematics.

[16] Karol Pa̧k. Stirling numbers of the second kind. Formalized Mathematics, 13(2):337–345, 2005.

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

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

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

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

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

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

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

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

[25] Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-based finite sequences. Formalized Mathematics, 9(4):825–829, 2001.

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

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

Some Equations Related to the Limit of Sequence of Subsets

Bo Zhang Shinshu University

Nagano, Japan Hiroshi Yamazaki Shinshu University Nagano, Japan Yatsuka Nakamura Shinshu University Nagano, Japan

Summary. Set operations for sequences of subsets are introduced here. Some relations for these operations with the limit of sequences of subsets, also with the inferior sequence and the superior sequence of sets, and with the inferior limit and the superior limit of sets are shown.

MML identifier: SETLIM 2, version: 7.5.01 4.39.921

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

For simplicity, we use the following convention: n, k denote natural numbers, X denotes a set, A denotes a subset of X, and A_{1}, A_{2} denote sequences of subsets of X.

We now state two propositions:

(1) (The inferior setsequence A_{1})(n) = Intersection(A_{1} ↑ n).

(2) (The superior setsequence A_{1})(n) = ⋃(A_{1} ↑ n).

Let us consider X and let A_{1}, A_{2} be sequences of subsets of X. The functor A_{1} ∩ A_{2} yields a sequence of subsets of X and is defined as follows:

(Def. 1) For every n holds (A_{1} ∩ A_{2})(n) = A_{1}(n) ∩ A_{2}(n). Let us note that the functor A_{1} ∩ A_{2} is commutative. The functor A_{1} ∪ A_{2} yielding a sequence of subsets of X is defined as follows:

(Def. 2) For every n holds (A_{1} ∪ A_{2})(n) = A_{1}(n) ∪ A_{2}(n). Let us observe that the functor A_{1} ∪ A_{2} is commutative. The functor A_{1} \ A_{2} yielding a sequence of subsets of X is defined by:

(Def. 3) For every n holds (A_{1} \ A_{2})(n) = A_{1}(n) \ A_{2}(n). The functor A_{1}− . A_{2} yields a sequence of subsets of X and is defined as follows:

(Def. 4) For every n holds (A_{1}− . A_{2})(n) = A_{1}(n)− . A_{2}(n).

Let us note that the functor A_{1}− . A_{2} is commutative.

One can prove the following propositions:

(3) A_{1}− . A_{2} = (A_{1} \ A_{2}) ∪ (A_{2} \ A_{1}).

(4) (A_{1} ∩ A_{2}) ↑ k = A_{1} ↑ k ∩ A_{2} ↑ k.

(5) (A_{1} ∪ A_{2}) ↑ k = A_{1} ↑ k ∪ A_{2} ↑ k.

(6) (A_{1} \ A_{2}) ↑ k = A_{1} ↑ k \ A_{2} ↑ k.

(7) (A_{1}− . A_{2}) ↑ k = A_{1} ↑ k− . A_{2} ↑ k.

(8) ⋃(A_{1} ∩ A_{2}) ⊆ ⋃ A_{1} ∩ ⋃ A_{2}.

(9) ⋃(A_{1} ∪ A_{2}) = ⋃ A_{1} ∪ ⋃ A_{2}.

(10) ⋃ A_{1} \ ⋃ A_{2} ⊆ ⋃(A_{1} \ A_{2}).

(11) ⋃ A_{1}− . ⋃ A_{2} ⊆ ⋃(A_{1}− . A_{2}).

(12) Intersection(A_{1} ∩ A_{2}) = Intersection A_{1} ∩ Intersection A_{2}.

(13) Intersection A_{1} ∪ Intersection A_{2} ⊆ Intersection(A_{1} ∪ A_{2}).

(14) Intersection(A_{1} \ A_{2}) ⊆ Intersection A_{1} \ Intersection A_{2}. Let us consider X, let A_{1} be a sequence of subsets of X, and let A be a

subset of X. The functor A ∩ A_{1} yielding a sequence of subsets of X is defined by:

(Def. 5) For every n holds (A ∩ A_{1})(n) = A ∩ A_{1}(n).

The functor A ∪ A_{1} yielding a sequence of subsets of X is defined as follows: (Def. 6) For every n holds (A ∪ A_{1})(n) = A ∪ A_{1}(n).

The functor A \ A_{1} yields a sequence of subsets of X and is defined by: (Def. 7) For every n holds (A \ A_{1})(n) = A \ A_{1}(n).

The functor A_{1} \ A yields a sequence of subsets of X and is defined by: (Def. 8) For every n holds (A_{1} \ A)(n) = A_{1}(n) \ A.

The functor A− . A_{1} yielding a sequence of subsets of X is defined as follows: (Def. 9) For every n holds (A− . A_{1})(n) = A− . A_{1}(n).

One can prove the following propositions:

(15) A− . A_{1} = (A \ A_{1}) ∪ (A_{1} \ A).

(16) (A ∩ A_{1}) ↑ k = A ∩ A_{1} ↑ k.

(17) (A ∪ A_{1}) ↑ k = A ∪ A_{1} ↑ k.

(18) (A \ A_{1}) ↑ k = A \ A_{1} ↑ k.

(19) (A_{1} \ A) ↑ k = A_{1} ↑ k \ A.

(20) (A− . A_{1}) ↑ k = A− . A_{1} ↑ k.

(21) If A_{1} is non-increasing, then A ∩ A_{1} is non-increasing.

(22) If A_{1} is non-decreasing, then A ∩ A_{1} is non-decreasing.

(23) If A_{1} is monotone, then A ∩ A_{1} is monotone.

(24) If A_{1} is non-increasing, then A ∪ A_{1} is non-increasing.

(25) If A_{1} is non-decreasing, then A ∪ A_{1} is non-decreasing.

(26) If A_{1} is monotone, then A ∪ A_{1} is monotone.

(27) If A_{1} is non-increasing, then A \ A_{1} is non-decreasing.

(28) If A_{1} is non-decreasing, then A \ A_{1} is non-increasing.

(29) If A_{1} is monotone, then A \ A_{1} is monotone.

(30) If A_{1} is non-increasing, then A_{1} \ A is non-increasing.

(31) If A_{1} is non-decreasing, then A_{1} \ A is non-decreasing.

(32) If A_{1} is monotone, then A_{1} \ A is monotone.

(33) Intersection(A ∩ A_{1}) = A ∩ Intersection A_{1}.

(34) Intersection(A ∪ A_{1}) = A ∪ Intersection A_{1}.

(35) Intersection(A \ A_{1}) ⊆ A \ Intersection A_{1}.

(36) Intersection(A_{1} \ A) = Intersection A_{1} \ A.

(37) Intersection(A− . A_{1}) ⊆ A− . Intersection A_{1}.

(38) ⋃(A ∩ A_{1}) = A ∩ ⋃ A_{1}.

(39) ⋃(A ∪ A_{1}) = A ∪ ⋃ A_{1}.

(40) A \ ⋃ A_{1} ⊆ ⋃(A \ A_{1}).

(41) ⋃(A_{1} \ A) = ⋃ A_{1} \ A.

(42) A− . ⋃ A_{1} ⊆ ⋃(A− . A_{1}).

(43) (The inferior setsequence A_{1} ∩ A_{2})(n) = (the inferior setsequence A_{1})(n) ∩ (the inferior setsequence A_{2})(n).

(44) (The inferior setsequence A_{1})(n)∪(the inferior setsequence A_{2})(n) ⊆ (the inferior setsequence A_{1} ∪ A_{2})(n).

(45) (The inferior setsequence A_{1}\A_{2})(n) ⊆ (the inferior setsequence A_{1})(n)\ (the inferior setsequence A_{2})(n).

(46) (The superior setsequence A_{1} ∩ A_{2})(n) ⊆ (the superior setsequence A_{1})(n) ∩ (the superior setsequence A_{2})(n).

(47) (The superior setsequence A_{1} ∪ A_{2})(n) = (the superior setsequence A_{1})(n) ∪ (the superior setsequence A_{2})(n).

(48) (The superior setsequence A_{1})(n) \ (the superior setsequence A_{2})(n) ⊆ (the superior setsequence A_{1} \ A_{2})(n).

(49) (The superior setsequence A_{1})(n)− . (the superior setsequence A_{2})(n) ⊆ (the superior setsequence A_{1}− . A_{2})(n).

(50) (The inferior setsequence A ∩ A_{1})(n) = A ∩ (the inferior setsequence A_{1})(n).

(51) (The inferior setsequence A ∪ A_{1})(n) = A ∪ (the inferior setsequence A_{1})(n).

(52) (The inferior setsequence A \ A_{1})(n) ⊆ A \ (the inferior setsequence A_{1})(n).

(53) (The inferior setsequence A_{1} \A)(n) = (the inferior setsequence A_{1})(n)\ A.

(54) (The inferior setsequence A− . A_{1})(n) ⊆ A− . (the inferior setsequence A_{1})(n).

(55) (The superior setsequence A ∩ A_{1})(n) = A ∩ (the superior setsequence A_{1})(n).

(56) (The superior setsequence A ∪ A_{1})(n) = A ∪ (the superior setsequence A_{1})(n).

(57) A \ (the superior setsequence A_{1})(n) ⊆ (the superior setsequence A \ A_{1})(n).

(58) (The superior setsequence A_{1} \ A)(n) = (the superior setsequence A_{1})(n) \ A.

(59) A− . (the superior setsequence A_{1})(n) ⊆ (the superior setsequence A− . A_{1})(n).

(60) lim inf(A_{1} ∩ A_{2}) = lim inf A_{1} ∩ lim inf A_{2}.

(61) lim inf A_{1} ∪ lim inf A_{2} ⊆ lim inf(A_{1} ∪ A_{2}).

(62) lim inf(A_{1} \ A_{2}) ⊆ lim inf A_{1} \ lim inf A_{2}.

(63) If A_{1} is convergent or A_{2} is convergent, then lim inf(A_{1} ∪ A_{2}) = lim inf A_{1} ∪ lim inf A_{2}.

(64) If A_{2} is convergent, then lim inf(A_{1} \ A_{2}) = lim inf A_{1} \ lim inf A_{2}.

(65) If A_{1} is convergent or A_{2} is convergent, then lim inf(A_{1}− . A_{2}) ⊆ lim inf A_{1}− . lim inf A_{2}.

(66) If A_{1} is convergent and A_{2} is convergent, then lim inf(A_{1}− . A_{2}) = lim inf A_{1}− . lim inf A_{2}.

(67) lim sup(A_{1} ∩ A_{2}) ⊆ lim sup A_{1} ∩ lim sup A_{2}.

(68) lim sup(A_{1} ∪ A_{2}) = lim sup A_{1} ∪ lim sup A_{2}.

(69) lim sup A_{1} \ lim sup A_{2} ⊆ lim sup(A_{1} \ A_{2}).

(70) lim sup A_{1}− . lim sup A_{2} ⊆ lim sup(A_{1}− . A_{2}).

(71) If A_{1} is convergent or A_{2} is convergent, then lim sup(A_{1} ∩ A_{2}) = lim sup A_{1} ∩ lim sup A_{2}.

(72) If A_{2} is convergent, then lim sup(A_{1} \ A_{2}) = lim sup A_{1} \ lim sup A_{2}.

(73) If A_{1} is convergent and A_{2} is convergent, then lim sup(A_{1}− . A_{2}) = lim sup A_{1}− . lim sup A_{2}.

(74) lim inf(A ∩ A_{1}) = A ∩ lim inf A_{1}.

(75) lim inf(A ∪ A_{1}) = A ∪ lim inf A_{1}.

(76) lim inf(A \ A_{1}) ⊆ A \ lim inf A_{1}.

(77) lim inf(A_{1} \ A) = lim inf A_{1} \ A.

(78) lim inf(A− . A_{1}) ⊆ A− . lim inf A_{1}.

(79) If A_{1} is convergent, then lim inf(A \ A_{1}) = A \ lim inf A_{1}.

(80) If A_{1} is convergent, then lim inf(A− . A_{1}) = A− . lim inf A_{1}.

(81) lim sup(A ∩ A_{1}) = A ∩ lim sup A_{1}.

(82) lim sup(A ∪ A_{1}) = A ∪ lim sup A_{1}.

(83) A \ lim sup A_{1} ⊆ lim sup(A \ A_{1}).

(84) lim sup(A_{1} \ A) = lim sup A_{1} \ A.

(85) A− . lim sup A_{1} ⊆ lim sup(A− . A_{1}).

(86) If A_{1} is convergent, then lim sup(A \ A_{1}) = A \ lim sup A_{1}.

(87) If A_{1} is convergent, then lim sup(A− . A_{1}) = A− . lim sup A_{1}.

(88) If A_{1} is convergent and A_{2} is convergent, then A_{1} ∩ A_{2} is convergent and lim(A_{1} ∩ A_{2}) = lim A_{1} ∩ lim A_{2}.

(89) If A_{1} is convergent and A_{2} is convergent, then A_{1} ∪ A_{2} is convergent and lim(A_{1} ∪ A_{2}) = lim A_{1} ∪ lim A_{2}.

(90) If A_{1} is convergent and A_{2} is convergent, then A_{1} \ A_{2} is convergent and lim(A_{1} \ A_{2}) = lim A_{1} \ lim A_{2}.

(91) If A_{1} is convergent and A_{2} is convergent, then A_{1}− . A_{2} is convergent and lim(A_{1}− . A_{2}) = lim A_{1}− . lim A_{2}.

(92) If A_{1} is convergent, then A ∩ A_{1} is convergent and lim(A ∩ A_{1}) = A ∩ lim A_{1}.

(93) If A_{1} is convergent, then A ∪ A_{1} is convergent and lim(A ∪ A_{1}) = A ∪ lim A_{1}.

(94) If A_{1} is convergent, then A\A_{1} is convergent and lim(A\A_{1}) = A\lim A_{1}.

(95) If A_{1} is convergent, then A_{1}\A is convergent and lim(A_{1}\A) = lim A_{1}\A.

(96) If A_{1} is convergent, then A− . A_{1} is convergent and lim(A− . A_{1}) = A− . lim A_{1}.

References

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

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

[3] Adam Grabowski. On the Kuratowski limit operators. Formalized Mathematics, 11(4):399– 409, 2003.

[4] Andrzej Nȩdzusiak. σ-fields and probability. Formalized Mathematics, 1(2):401–407, 1990.

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

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

412 bo zhang et al.

[7] Bo Zhang, Hiroshi Yamazaki, and Yatsuka Nakamura. Limit of sequence of subsets. For-

malized Mathematics, 13(2):347–352, 2005.

Received May 24, 2005

On the Partial Product of Series and Related Basic Inequalities

Fuguo Ge

Qingdao University of Science

and Technology China

Xiquan Liang Qingdao University of Science and Technology China

Summary. This article describes definition of partial product of series, introduced similarly to its related partial sum, as well as several important inequalities true for chosen special series.

MML identifier: SERIES 3, version: 7.5.01 4.39.921

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

For simplicity, we adopt the following convention: a, b, c are positive real numbers, m, x, y, z are real numbers, n is a natural number, and s, s_{1}, s_{2}, s_{3}, s_{4}, s_{5} are sequences of real numbers.

Let us consider x. Note that |x| is non negative. We now state a number of propositions:

(1) If y > x and x ≥ 0 and m ≥ 0, then \frac{x}{y} ≤ \frac{x+m}{y+m}.

(2) \frac{a+b}{2} ≥ \sqrt{a · b}.

(3) \frac{b}{a} + \frac{a}{b} ≥ 2.

(4) (\frac{x+y}{2} )^{2} ≥ x · y.

(5) \frac{x^{2}+y^{2}}{2} ≥ (\frac{x+y}{2} )^{2}.

(6) x^{2} + y^{2} ≥ 2 · x · y.

(7) \frac{x^{2}+y^{2}}{2} ≥ x · y.

(8) x^{2} + y^{2} ≥ 2 · |x| · |y|.

(9) (x + y)^{2} ≥ 4 · x · y.

(10) x^{2} + y^{2} + z^{2} ≥ x · y + y · z + x · z.

(11) (x + y + z)^{2} ≥ 3 · (x · y + y · z + x · z).

(12) a^{3} + b^{3} + c^{3} ≥ 3 · a · b · c.

(13) \frac{a^{3}+b^{3}+c^{3}}{3} ≥ a · b · c.

(14) (\frac{a}{b})^{3} + (\frac{b}{c})^{3} + (\frac{c}{a})^{3} ≥ \frac{b}{a} + \frac{c}{b} + \frac{a}{c}.

(15) a + b + c ≥ 3 · ^{3} \sqrt{a · b · c}.

(16) \frac{a+b+c}{3} ≥ ^{3} \sqrt{a · b · c}.

(17) If x + y + z = 1, then x · y + y · z + x · z ≤ \frac{1}{3}.

(18) If x + y = 1, then x · y ≤ \frac{1}{4}.

(19) If x + y = 1, then x^{2} + y^{2} ≥ \frac{1}{2}.

(20) If a + b = 1, then (1 + \frac{1}{a}) · (1 + \frac{1}{b}) ≥ 9.

(21) If x + y = 1, then x^{3} + y^{3} ≥ \frac{1}{4}.

(22) If a + b = 1, then a^{3} + b^{3} < 1.

(23) If a + b = 1, then (a + \frac{1}{a}) · (b + \frac{1}{b}) ≥ \frac{25}{4}.

(24) If |x| ≤ a, then x^{2} ≤ a^{2}.

(25) If |x| ≥ a, then x^{2} ≥ a^{2}.

(26) ||x| − |y|| ≤ |x| + |y|.

(27) If a · b · c = 1, then \frac{1}{a} + \frac{1}{b} + \frac{1}{c} ≥ \sqrt{a} + \sqrt{b} + \sqrt{c}.

(28) If x > 0 and y > 0 and z < 0 and x + y + z = 0, then (x^{2} + y^{2} + z^{2})^{3} ≥ 6 · (x^{3} + y^{3} + z^{3})^{2}.

(29) If a ≥ 1, then a^{b} + a^{c} ≥ 2 · a^{\sqrt{b·c}}.

(30) If a ≥ b and b ≥ c, then a^{a} · b^{b} · c^{c} ≥ (a · b · c)^{\frac{a+b+c}{3}} .

(31) (a + b)^{n+2} ≥ a^{n+2} + (n + 2) · a^{n+1} · b.

(32) \frac{a^{n}+b^{n}}{2} ≥ (\frac{a+b}{2})^{n}.

(33) If for every n holds s(n) > 0, then for every n holds (∑_{α=0}^{κ} s(α))_{κ∈ℕ}(n) > 0.

(34) If for every n holds s(n) ≥ 0, then for every n holds (∑_{α=0}^{κ} s(α))_{κ∈ℕ}(n) ≥ 0.

(35) If for every n holds s(n) < 0, then (∑_{α=0}^{κ} s(α))_{κ∈ℕ}(n) < 0.

(36) If s = s_{1} s_{1}, then for every n holds (∑_{α=0}^{κ} s(α))_{κ∈ℕ}(n) ≥ 0.

(37) If for every n holds s(n) > 0 and s(n) > s(n−1), then (n+1)·s(n+1) > (∑_{α=0}^{κ} s(α))_{κ∈ℕ}(n).

(38) If s = s_{1} s_{2} and for every n holds s_{1}(n) ≥ 0 and s_{2}(n) ≥ 0, then for every n holds (∑_{α=0}^{κ} s(α))_{κ∈ℕ}(n) ≤ (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(n) · (∑_{α=0}^{κ}(s_{2})(α))_{κ∈ℕ}(n).

(39) If s = s_{1} s_{2} and for every n holds s_{1}(n) < 0 and s_{2}(n) < 0, then (∑_{α=0}^{κ} s(α))_{κ∈ℕ}(n) ≤ (∑_{α=0}^{κ}(s_{1})(α))_{κ∈ℕ}(n) · (∑_{α=0}^{κ}(s_{2})(α))_{κ∈ℕ}(n).

(40) For every n holds |(∑_{α=0}^{κ} s(α))_{κ∈ℕ}(n)| ≤ (∑_{α=0}^{κ}|s|(α))_{κ∈ℕ}(n).

(41) (∑_{α=0}^{κ} s(α))_{κ∈ℕ}(n) ≤ (∑_{α=0}^{κ}|s|(α))_{κ∈ℕ}(n).

Let us consider s. The partial product of s yielding a sequence of real numbers is defined by the conditions (Def. 1).

(Def. 1)(i) (The partial product of s)(0) = s(0), and

(ii) for every n holds (the partial product of s)(n+1) = (the partial product

of s)(n) · s(n + 1). We now state a number of propositions:

(42) If for every n holds s(n) > 0, then (the partial product of s)(n) > 0.

(43) If for every n holds s(n) ≥ 0, then (the partial product of s)(n) ≥ 0.

(44) Suppose that for every n holds s(n) > 0 and s(n) < 1. Let given n. Then (the partial product of s)(n) > 0 and (the partial product of s)(n) < 1.

(45) If for every n holds s(n) ≥ 1, then for every n holds (the partial product of s)(n) ≥ 1.

(46) Suppose that for every n holds s_{1}(n) ≥ 0 and s_{2}(n) ≥ 0. Let given n. Then (the partial product of s_{1})(n)+(the partial product of s_{2})(n) ≤ (the partial product of s_{1} + s_{2})(n).

(47) If for every n holds s(n) = \frac{2·n+1}{2·n+2}, then (the partial product of s)(n) ≤ \frac{1}{\sqrt{3·n+4}}.

(48) If for every n holds s_{1}(n) = 1 + s(n) and s(n) > −1 and s(n) < 0, then for every n holds 1 + (∑_{α=0}^{κ} s(α))_{κ∈ℕ}(n) ≤ (the partial product of s_{1})(n).

(49) If for every n holds s_{1}(n) = 1+s(n) and s(n) ≥ 0, then for every n holds 1 + (∑_{α=0}^{κ} s(α))_{κ∈ℕ}(n) ≤ (the partial product of s_{1})(n).

(50) If s_{3} = s_{1} s_{2} and s_{4} = s_{1} s_{1} and s_{5} = s_{2} s_{2}, then for every n holds (∑_{α=0}^{κ}(s_{3})(α))_{κ∈ℕ}(n)^{2} ≤ (∑_{α=0}^{κ}(s_{4})(α))_{κ∈ℕ}(n) · (∑_{α=0}^{κ}(s_{5})(α))_{κ∈ℕ}(n).

(51) If s_{4} = s_{1} s_{1} and s_{5} = s_{2} s_{2} and for every n holds s_{1}(n) ≥ 0 and s_{2}(n) ≥ 0 and s_{3}(n) = (s_{1}(n) + s_{2}(n))^{2}, then for every n holds \sqrt{(∑_{α=0}^{κ}(s_{3})(α))_{κ∈ℕ}(n)} ≤ \sqrt{(∑_{α=0}^{κ}(s_{4})(α))_{κ∈ℕ}(n)} + \sqrt{(∑_{α=0}^{κ}(s_{5})(α))_{κ∈ℕ}(n)}.

(52) If for every n holds s(n) > 0 and s(n) > s(n − 1), then (∑_{α=0}^{κ} s(α))_{κ∈ℕ}(n) ≥ (n + 1) · ^{n+1} \sqrt{(the partial product of s)(n)}.

References

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

[2] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 1990.

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

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

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

[6] Library Committee of the Association of Mizar Users. Binary operations on numbers. To appear in Formalized Mathematics.

416 fuguo ge and xiquan liang

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

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

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

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

Homeomorphism between Finite Topological Spaces, Two-Dimensional

Lattice Spaces and a Fixed Point Theorem

Masami Tanaka Shinshu University

Nagano, Japan

Hiroshi Imura Shinshu University Nagano, Japan Yatsuka Nakamura Shinshu University Nagano, Japan

Summary. In this paper we first introduced the notion of homeomorphism between finite topological spaces. We also gave a fixed point theorem in finite topological space. Next, we showed two 2-dimensional concrete models of lattice spaces. One was 2-dimensional linear finite topological space. Another was 2dimensional small finite topological space.

      MML identifier: FINTOPO5, version: 7.5.01 4.39.921

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

The following propositions are true:

(1) Let X be a set, Y be a non empty set, f be a function from X into Y, and A be a subset of X. If f is one-to-one, then (f^{−1})^{∘}f^{∘}A = A.

(2) For every natural number n holds n > 0 iff Seg n ≠ ∅.

Let F_{1}, F_{2} be finite topology spaces and let h be a map from F_{1} into F_{2}. We say that h is a homeomorphism if and only if the conditions (Def. 1) are satisfied.

(Def. 1)(i) h is one-to-one and onto, and

(ii) for every element x of F_{1} holds h^{∘}(the neighbour-map of F_{1})(x) = (the

neighbour-map of F_{2})(h(x)). One can prove the following propositions:

(3) Let F_{1}, F_{2} be non empty finite topology spaces and h be a map from F_{1} into F_{2}. Suppose h is a homeomorphism. Then there exists a map g from F_{2} into F_{1} such that g = h^{−1} and g is a homeomorphism.

(4) Let F_{1}, F_{2} be non empty finite topology spaces, h be a map from F_{1} into F_{2}, n be a natural number, x be an element of F_{1}, and y be an element of F_{2}. Suppose h is a homeomorphism and y = h(x). Let z be an element of F_{1}. Then z ∈ U(x, n) if and only if h(z) ∈ U(y, n).

(5) Let F_{1}, F_{2} be non empty finite topology spaces, h be a map from F_{1} into F_{2}, n be a natural number, x be an element of F_{1}, and y be an element of F_{2}. Suppose h is a homeomorphism and y = h(x). Let v be an element of F_{2}. Then h^{−1}(v) ∈ U(x, n) if and only if v ∈ U(y, n).

(6) Let n be a non zero natural number and f be a map from FTSL1(n) into FTSL1(n). If f is continuous 0, then there exists an element p of FTSL1(n) such that f(p) ∈ U(p, 0).

(7) Let T be a non empty finite topology space, p be an element of T, and k be a natural number. If T is filled, then U(p, k) ⊆ U(p, k + 1).

(8) Let T be a non empty finite topology space, p be an element of T, and k be a natural number. If T is filled, then U(p, 0) ⊆ U(p, k).

(9) Let n be a non zero natural number, j_{1}, j, k be natural numbers, and p be an element of FTSL1(n). If p = j_{1}, then j ∈ U(p, k) iff j ∈ Seg n and |j_{1} − j| ≤ k + 1.

(10) Let k_{1}, k_{2} be natural numbers, n be a non zero natural number, and f be a map from FTSL1(n) into FTSL1(n). Suppose f is continuous k_{1} and k_{2} = ⌈\frac{k_{1}}{2} ⌉. Then there exists an element p of FTSL1(n) such that f(p) ∈ U(p, k_{2}).

Let n, m be natural numbers. The functor Nbdl2(n, m) yields a function from [: Seg n, Seg m:] into 2^{[: Seg n, Seg m:]} and is defined by:

(Def. 2) For every set x such that x ∈ [: Seg n, Seg m:] and for all natural numbers i, j such that x = ⟨⟨i, j⟩⟩ holds (Nbdl2(n, m))(x) = [: (Nbdl1(n))(i), (Nbdl1(m))(j) :].

Let n, m be natural numbers. The functor FTSL2(n, m) yielding a strict finite topology space is defined as follows:

(Def. 3) FTSL2(n, m) = ⟨[: Seg n, Seg m:], Nbdl2(n, m)⟩.

Let n, m be non zero natural numbers. One can verify that FTSL2(n, m) is non empty.

We now state three propositions:

(11) For all non zero natural numbers n, m holds FTSL2(n, m) is filled.

(12) For all non zero natural numbers n, m holds FTSL2(n, m) is symmetric.

(13) For every non zero natural number n holds there exists a map from

FTSL2(n, 1) into FTSL1(n) which is a homeomorphism. Let n, m be natural numbers. The functor Nbds2(n, m) yielding a function

from [: Seg n, Seg m:] into 2^{[: Seg n, Seg m:]} is defined by:

homeomorphism between finite topological … 419

(Def. 4) For every set x such that x ∈ [: Seg n, Seg m:] and for all natural numbers i, j such that x = ⟨⟨i, j⟩⟩ holds (Nbds2(n, m))(x) = [: {i}, (Nbdl1(m))(j) :]∪ [: (Nbdl1(n))(i), {j}:].

Let n, m be natural numbers. The functor FTSS2(n, m) yielding a strict finite topology space is defined as follows:

(Def. 5) FTSS2(n, m) = ⟨[: Seg n, Seg m:], Nbds2(n, m)⟩.

Let n, m be non zero natural numbers. Note that FTSS2(n, m) is non empty. One can prove the following propositions:

(14) For all non zero natural numbers n, m holds FTSS2(n, m) is filled.

(15) For all non zero natural numbers n, m holds FTSS2(n, m) is symmetric.

(16) For every non zero natural number n holds there exists a map from FTSS2(n, 1) into FTSL1(n) which 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] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 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. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.

[7] Hiroshi Imura and Masayoshi Eguchi. Finite topological spaces. Formalized Mathematics, 3(2):189–193, 1992.

[8] Hiroshi Imura, Masami Tanaka, and Yatsuka Nakamura. Continuous mappings between finite and one-dimensional finite topological spaces. Formalized Mathematics, 12(3):381– 384, 2004.

[9] Masami Tanaka and Yatsuka Nakamura. Some set series in finite topological spaces. Fundamental concepts for image processing. Formalized Mathematics, 12(2):125–129, 2004.

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

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

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

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

420 masami tanaka et al.

The Maclaurin Expansions

Akira Nishino Shinshu University Nagano, Japan Yasunari Shidama Shinshu University Nagano, Japan

Summary. A concept of the Maclaurin expansions is defined here. This article contains the definition of the Maclaurin expansion and expansions of exp, sin and cos functions.

MML identifier: TAYLOR 2, version: 7.5.01 4.39.921

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

The following proposition is true

(1) For every real number x and for every natural number n holds |x^{n}| = |x|^{n}.

Let f be a partial function from ℝ to ℝ, let Z be a subset of ℝ, and let a be a real number. The functor Maclaurin(f, Z, a) yields a sequence of real numbers and is defined by:

(Def. 1) Maclaurin(f, Z, a) = Taylor(f, Z, 0, a). The following propositions are true:

(2) Let n be a natural number, f be a partial function from ℝ to ℝ, and r be a real number. Suppose 0 < r and f is differentiable n + 1 times on ]−r, r[. Let x be a real number. Suppose x ∈ ]−r, r[. Then there exists a real number s such that 0 < s and s < 1 and f(x) = (∑_{α=0}^{κ}(Maclaurin(f,]−r, r[, x))(α))_{κ∈ℕ}(n) + \frac{f′(]−r,r[)(n+1)(s·x)·x^{n+1}}{(n+1)!} .

(3) Let n be a natural number, f be a partial function from ℝ to ℝ, and x_{0}, r be real numbers. Suppose 0 < r and f is differentiable n + 1 times on ]x_{0} − r, x_{0} + r[. Let x be a real number. Suppose x ∈ ]x_{0} − r, x_{0} + r[. Then there exists a real number s such that 0 < s and s < 1 and |f(x) − (∑_{α=0}^{κ}(Taylor(f,]x_{0} − r, x_{0} + r[, x_{0}, x))(α))_{κ∈ℕ}(n)| = |\frac{f′(]x_{0}−r,x_{0}+r[)(n+1)(x_{0}+s·(x−x_{0}))·(x−x_{0})^{n+1}}{(n+1)!} |.

(4) Let n be a natural number, f be a partial function from ℝ to ℝ, and r be a real number. Suppose 0 < r and f is differentiable n + 1 times on ]−r, r[. Let x be a real number. Suppose x ∈ ]−r, r[. Then there exists a real number s such that 0 < s and s < 1 and |f(x) − (∑_{α=0}^{κ}(Maclaurin(f,]−r, r[, x))(α))_{κ∈ℕ}(n)| = |\frac{f′(]−r,r[)(n+1)(s·x)·x^{n+1}}{(n+1)!} |.

(5) For every real number r holds exp′_{↾]−r,r[} = exp ↾]−r, r[ and dom(exp ↾]−r, r[) = ]−r, r[.

(6) For every natural number n and for every real number r holds exp′(]−r, r[)(n) = exp ↾]−r, r[.

(7) For every natural number n and for all real numbers r, x such that x ∈ ]−r, r[ holds exp′(]−r, r[)(n)(x) = exp(x).

(8) For every natural number n and for all real numbers r, x such that 0 < r holds (Maclaurin(exp,]−r, r[, x))(n) = \frac{x^{n}}{n!} .

(9) Let n be a natural number and r, x, s be real numbers. Suppose x ∈ ]−r, r[ and 0 < s and s < 1. Then |\frac{exp′(]−r,r[)(n+1)(s·x)·x^{n+1}}{(n+1)!} | ≤

\frac{|exp(s·x)|·|x|^{n+1}}{(n+1)!} .

(10) For every real number r and for every natural number n holds exp is differentiable n times on ]−r, r[.

(11) Let r be a real number. Suppose 0 < r. Then there exist real numbers

M, L such that

(i) 0 ≤ M, (ii) 0 ≤ L, and (iii) for every natural number n and for all real numbers x, s such that

x ∈ ]−r, r[ and 0 < s and s < 1 holds |\frac{exp′(]−r,r[)(n)(s·x)·x^{n}}{n!} | ≤ \frac{M·L^{n}}{n!} .

(12) Let M, L be real numbers. Suppose M ≥ 0 and L ≥ 0. Let e be a real number. Suppose e > 0. Then there exists a natural number n such that for every natural number m if n ≤ m, then \frac{M·L^{m}}{m!} < e.

(13) Let r, e be real numbers. Suppose 0 < r and 0 < e. Then there exists a natural number n such that for every natural number m if n ≤ m, then for all real numbers x, s such that x ∈ ]−r, r[ and 0 < s and s < 1 holds |\frac{exp′(]−r,r[)(m)(s·x)·x^{m}}{m!} | < e.

(14) Let r, e be real numbers. Suppose 0 < r and 0 < e. Then there exists a natural number n such that for every natural number m if n ≤ m, then for every real number x such that x ∈ ]−r, r[ holds |exp(x) − (∑_{α=0}^{κ}(Maclaurin(exp,]−r, r[, x))(α))_{κ∈ℕ}(m)| < e.

(15) For every real number x holds x ExpSeq is absolutely summable.

(16) For all real numbers r, x such that 0 < r holds Maclaurin(exp,]−r, r[, x) = x ExpSeq and Maclaurin(exp,]−r, r[, x) is absolutely summable and exp(x) = ∑ Maclaurin(exp,]−r, r[, x).

(17) Let r be a real number. Then (i) (the function sin)′_{↾]−r,r[} = (the function cos)↾]−r, r[, (ii) (the function cos)′_{↾]−r,r[} = (−the function sin)↾]−r, r[, (iii) dom((the function sin)↾]−r, r[) = ]−r, r[, and (iv) dom((the function cos)↾]−r, r[) = ]−r, r[.

(18) Let f be a partial function from ℝ to ℝ and Z be a subset of ℝ. If f is differentiable on Z, then (−f)′_{↾Z} = −f′_{↾Z}.

(19) Let r be a real number and n be a natural number. Then (i) (the function sin)′(]−r, r[)(2 · n) = (−1)^{n} ((the function sin)↾]−r, r[), (ii) (the function sin)′(]−r, r[)(2·n+1) = (−1)^{n} ((the function cos)↾]−r, r[), (iii) (the function cos)′(]−r, r[)(2 · n) = (−1)^{n} ((the function cos)↾]−r, r[),

and (iv) (the function cos)′(]−r, r[)(2 · n + 1) = (−1)^{n+1} ((the function

sin)↾]−r, r[).

(20) Let n be a natural number and r, x be real numbers. Suppose r > 0.

Then

(i) (Maclaurin(the function sin,]−r, r[, x))(2 · n) = 0, (ii) (Maclaurin(the function sin,]−r, r[, x))(2 · n + 1) = \frac{(−1)^{n}·x^{2·n+1}}{(2·n+1)!} ,

(iii) (Maclaurin(the function cos,]−r, r[, x))(2 · n) = \frac{(−1)^{n}·x^{2·n}}{(2·n)!} , and (iv) (Maclaurin(the function cos,]−r, r[, x))(2 · n + 1) = 0.

(21) Let r be a real number and n be a natural number. Then the function sin is differentiable n times on ]−r, r[ and the function cos is differentiable n times on ]−r, r[.

(22) Let r be a real number. Suppose r > 0. Then there exist real numbers

r_{1}, r_{2} such that

(i) r_{1} ≥ 0, (ii) r_{2} ≥ 0, and (iii) for every natural number n and for all real numbers x, s such that x ∈

]−r, r[ and 0 < s and s < 1 holds |\frac{(the function sin)′(]−r,r[)(n)(s·x)·x^{n}}{n!} | ≤ \frac{r_{1}·r_{2}^{n}}{n!} and |\frac{(the function cos)′(]−r,r[)(n)(s·x)·x^{n}}{n!} | ≤ \frac{r_{1}·r_{2}^{n}}{n!} .

(23) Let r, e be real numbers. Suppose 0 < r and 0 < e. Then there exists a natural number n such that for every natural number m if n ≤ m, then for all real numbers x, s such that x ∈ ]−r, r[ and 0 < s and s < 1 holds |\frac{(the function sin)′(]−r,r[)(m)(s·x)·x^{m}}{m!} | < e and |\frac{(the function cos)′(]−r,r[)(m)(s·x)·x^{m}}{m!} | < e.

(24) Let r, e be real numbers. Suppose 0 < r and 0 < e. Then there exists a natural number n such that for every natural number m if n ≤ m, then for every real number x such that x ∈ ]−r, r[ holds |(the function sin)(x) − (∑_{α=0}^{κ}(Maclaurin(the func-424 akira nishino and yasunari shidama

tion sin,]−r, r[, x))(α))_{κ∈ℕ}(m)| < e and |(the function cos)(x) − (∑_{α=0}^{κ}(Maclaurin(the function cos,]−r, r[, x))(α))_{κ∈ℕ}(m)| < e.

(25) Let r, x be real numbers and m be a natural number. Suppose 0 < r. Then (∑_{α=0}^{κ}(Maclaurin(the function sin,]−r, r[, x))(α))_{κ∈ℕ}(2 · m + 1) = (∑_{α=0}^{κ} x P sin(α))_{κ∈ℕ}(m) and (∑_{α=0}^{κ}(Maclaurin(the function cos,]−r, r[, x))(α))_{κ∈ℕ}(2 · m + 1) = (∑_{α=0}^{κ} x P cos(α))_{κ∈ℕ}(m).

(26) Let r, x be real numbers and m be a natural number. Suppose 0 < r and m > 0. Then (∑_{α=0}^{κ}(Maclaurin(the function sin,]−r, r[, x))(α))_{κ∈ℕ}(2· m) = (∑_{α=0}^{κ} x P sin(α))_{κ∈ℕ}(m − 1) and (∑_{α=0}^{κ}(Maclaurin(the function cos,]−r, r[, x))(α))_{κ∈ℕ}(2 · m) = (∑_{α=0}^{κ} x P cos(α))_{κ∈ℕ}(m).

(27) Let r, x be real numbers and m be a natural number. If 0 < r, then (∑_{α=0}^{κ}(Maclaurin(the function cos,]−r, r[, x))(α))_{κ∈ℕ}(2 · m) = (∑_{α=0}^{κ} x P cos(α))_{κ∈ℕ}(m).

(28) Let r, x be real numbers. Suppose r > 0. Then (i) (∑_{α=0}^{κ}(Maclaurin(the function sin,]−r, r[, x))(α))_{κ∈ℕ} is convergent, (ii) (the function sin)(x) = ∑ Maclaurin(the function sin,]−r, r[, x), (iii) (∑_{α=0}^{κ}(Maclaurin(the function cos,]−r, r[, x))(α))_{κ∈ℕ} is convergent,

and (iv) (the function cos)(x) = ∑ Maclaurin(the function cos,]−r, r[, x).

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] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 1990.

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

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

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

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

[8] Beata Perkowska. Functional sequence from a domain to a domain. Formalized Mathematics, 3(1):17–21, 1992.

[9] Konrad Raczkowski. Integer and rational exponents. Formalized Mathematics, 2(1):125– 130, 1991.

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

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

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

[13] Yasunari Shidama. The Taylor expansions. Formalized Mathematics, 12(2):195–200, 2004.

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

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

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

the maclaurin expansions 425

[17] Yuguang Yang and Yasunari Shidama. Trigonometric functions and existence of circle

ratio. Formalized Mathematics, 7(2):255–263, 1998.

Received July 6, 2005 426 akira nishino and yasunari shidama

Several Differentiable Formulas of Special Functions

Yan Zhang

Qingdao University of Science

and Technology China

Xiquan Liang Qingdao University of Science and Technology China

Summary. In this article, we give several differentiable formulas of special functions. There are some specific composite functions consisting of rational functions, irrational functions, trigonometric functions, exponential functions or logarithmic functions.

MML identifier: FDIFF 4, version: 7.5.01 4.39.921

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

For simplicity, we follow the rules: x, a, b, c denote real numbers, n denotes a natural number, Z denotes an open subset of ℝ, and f, f_{1}, f_{2} denote partial functions from ℝ to ℝ.

One can prove the following propositions:

(1) Suppose Z ⊆ dom(log (e) · f) and for every x such that x ∈ Z holds f(x) = a + x and f(x) > 0. Then log (e) · f is differentiable on Z and for every x such that x ∈ Z holds (log (e) · f)′_{↾Z}(x) = \frac{1}{a+x}.

(2) Suppose Z ⊆ dom(log (e) · f) and for every x such that x ∈ Z holds f(x) = x − a and f(x) > 0. Then log (e) · f is differentiable on Z and for every x such that x ∈ Z holds (log (e) · f)′_{↾Z}(x) = \frac{1}{x−a}.

(3) Suppose Z ⊆ dom(−log (e) · f) and for every x such that x ∈ Z holds f(x) = a − x and f(x) > 0. Then −log (e) · f is differentiable on Z and for every x such that x ∈ Z holds (−log (e) · f)′_{↾Z}(x) = \frac{1}{a−x}.

(4) Suppose Z ⊆ dom(id_{Z}−a f) and f = log (e)·f_{1} and for every x such that x ∈ Z holds f_{1}(x) = a + x and f_{1}(x) > 0. Then id_{Z} − a f is differentiable on Z and for every x such that x ∈ Z holds (id_{Z} − a f)′_{↾Z}(x) = \frac{x}{a+x}.

(5) Suppose Z ⊆ dom((2 · a) f − id_{Z}) and f = log (e) · f_{1} and for every x such that x ∈ Z holds f_{1}(x) = a + x and f_{1}(x) > 0. Then (2 · a) f − id_{Z} is differentiable on Z and for every x such that x ∈ Z holds ((2 · a) f − id_{Z})′_{↾Z}(x) = \frac{a−x}{a+x}.

(6) Suppose Z ⊆ dom(id_{Z} − (2 · a) f) and f = log (e) · f_{1} and for every x such that x ∈ Z holds f_{1}(x) = x + a and f_{1}(x) > 0. Then id_{Z} − (2 · a) f is differentiable on Z and for every x such that x ∈ Z holds (id_{Z} − (2 · a) f)′_{↾Z}(x) = \frac{x−a}{x+a}.

(7) Suppose Z ⊆ dom(id_{Z} + (2 · a) f) and f = log (e) · f_{1} and for every x such that x ∈ Z holds f_{1}(x) = x − a and f_{1}(x) > 0. Then id_{Z} + (2 · a) f is differentiable on Z and for every x such that x ∈ Z holds (id_{Z} + (2 · a) f)′_{↾Z}(x) = \frac{x+a}{x−a}.

(8) Suppose Z ⊆ dom(id_{Z} + (a − b) f) and f = log (e) · f_{1} and for every x such that x ∈ Z holds f_{1}(x) = x + b and f_{1}(x) > 0. Then id_{Z} + (a − b) f is differentiable on Z and for every x such that x ∈ Z holds (id_{Z} + (a − b) f)′_{↾Z}(x) = \frac{x+a}{x+b}.

(9) Suppose Z ⊆ dom(id_{Z} + (a + b) f) and f = log (e) · f_{1} and for every x such that x ∈ Z holds f_{1}(x) = x − b and f_{1}(x) > 0. Then id_{Z} + (a + b) f is differentiable on Z and for every x such that x ∈ Z holds (id_{Z} + (a + b) f)′_{↾Z}(x) = \frac{x+a}{x−b}.

(10) Suppose Z ⊆ dom(id_{Z} − (a + b) f) and f = log (e) · f_{1} and for every x such that x ∈ Z holds f_{1}(x) = x + b and f_{1}(x) > 0. Then id_{Z} − (a + b) f is differentiable on Z and for every x such that x ∈ Z holds (id_{Z} − (a + b) f)′_{↾Z}(x) = \frac{x−a}{x+b}.

(11) Suppose Z ⊆ dom(id_{Z} + (b − a) f) and f = log (e) · f_{1} and for every x such that x ∈ Z holds f_{1}(x) = x − b and f_{1}(x) > 0. Then id_{Z} + (b − a) f is differentiable on Z and for every x such that x ∈ Z holds (id_{Z} + (b − a) f)′_{↾Z}(x) = \frac{x−a}{x−b}.

(12) Suppose Z ⊆ dom(f_{1} + c f_{2}) and for every x such that x ∈ Z holds f_{1}(x) = a + b · x and f_{2} = _{ℤ}^{2}. Then f_{1} + c f_{2} is differentiable on Z and for every x such that x ∈ Z holds (f_{1} + c f_{2})′_{↾Z}(x) = b + 2 · c · x.

(13) Suppose Z ⊆ dom(log (e) · (f_{1} + c f_{2})) and f_{2} = _{ℤ}^{2} and for every x such that x ∈ Z holds f_{1}(x) = a + b · x and (f_{1} + c f_{2})(x) > 0. Then log (e) · (f_{1} + c f_{2}) is differentiable on Z and for every x such that x ∈ Z holds (log (e) · (f_{1} + c f_{2}))′_{↾Z}(x) = \frac{b+2·c·x}{a+b·x+c·x^{2}} .

(14) Suppose Z ⊆ dom f and for every x such that x ∈ Z holds f(x) = a + x and f(x) ≠ 0. Then \frac{1}{f} is differentiable on Z and for every x such that

x ∈ Z holds (\frac{1}{f})′_{↾Z}(x) = −\frac{1}{(a+x)^{2}} .

(15) Suppose Z ⊆ dom((−1) \frac{1}{f}) and for every x such that x ∈ Z holds f(x) = a + x and f(x) ≠ 0. Then (−1) \frac{1}{f} is differentiable on Z and for every x such that x ∈ Z holds ((−1) \frac{1}{f})′_{↾Z}(x) = \frac{1}{(a+x)^{2}} .

(16) Suppose Z ⊆ dom f and for every x such that x ∈ Z holds f(x) = a − x and f(x) ≠ 0. Then \frac{1}{f} is differentiable on Z and for every x such that x ∈ Z holds (\frac{1}{f})′_{↾Z}(x) = \frac{1}{(a−x)^{2}} .

(17) Suppose Z ⊆ dom(f_{1} + f_{2}) and for every x such that x ∈ Z holds f_{1}(x) = a^{2} and f_{2} = _{ℤ}^{2}. Then f_{1} + f_{2} is differentiable on Z and for every x such that x ∈ Z holds (f_{1} + f_{2})′_{↾Z}(x) = 2 · x.

(18) Suppose Z ⊆ dom(log (e) · (f_{1} + f_{2})) and f_{2} = _{ℤ}^{2} and for every x such that x ∈ Z holds f_{1}(x) = a^{2} and (f_{1} + f_{2})(x) > 0. Then log (e) · (f_{1} + f_{2}) is differentiable on Z and for every x such that x ∈ Z holds (log (e) · (f_{1} + f_{2}))′_{↾Z}(x) = \frac{2·x}{a^{2}+x^{2}} .

(19) Suppose Z ⊆ dom(−log (e) · (f_{1} − f_{2})) and f_{2} = _{ℤ}^{2} and for every x such that x ∈ Z holds f_{1}(x) = a^{2} and (f_{1} − f_{2})(x) > 0. Then −log (e) · (f_{1} − f_{2}) is differentiable on Z and for every x such that x ∈ Z holds (−log (e) · (f_{1} − f_{2}))′_{↾Z}(x) = \frac{2·x}{a^{2}−x^{2}} .

(20) Suppose Z ⊆ dom(f_{1} + f_{2}) and for every x such that x ∈ Z holds f_{1}(x) = a and f_{2} = _{ℤ}^{3}. Then f_{1} + f_{2} is differentiable on Z and for every x such that x ∈ Z holds (f_{1} + f_{2})′_{↾Z}(x) = 3 · x^{2}.

(21) Suppose Z ⊆ dom(log (e) · (f_{1} + f_{2})) and f_{2} = _{ℤ}^{3} and for every x such that x ∈ Z holds f_{1}(x) = a and (f_{1} + f_{2})(x) > 0. Then log (e) · (f_{1} + f_{2}) is differentiable on Z and for every x such that x ∈ Z holds (log (e) · (f_{1} + f_{2}))′_{↾Z}(x) = \frac{3·x^{2}}{a+x^{3}} .

(22) Suppose Z ⊆ dom(log (e) · \frac{f_{1}}{f_{2}} ) and for every x such that x ∈ Z holds f_{1}(x) = a + x and f_{1}(x) > 0 and f_{2}(x) = a − x and f_{2}(x) > 0. Then log (e) · \frac{f_{1}}{f_{2}} is differentiable on Z and for every x such that x ∈ Z holds (log (e) · \frac{f_{1}}{f_{2}} )′_{↾Z}(x) = \frac{2·a}{a^{2}−x^{2}} .

(23) Suppose Z ⊆ dom(log (e) · \frac{f_{1}}{f_{2}} ) and for every x such that x ∈ Z holds f_{1}(x) = x − a and f_{1}(x) > 0 and f_{2}(x) = x + a and f_{2}(x) > 0. Then log (e) · \frac{f_{1}}{f_{2}} is differentiable on Z and for every x such that x ∈ Z holds (log (e) · \frac{f_{1}}{f_{2}} )′_{↾Z}(x) = \frac{2·a}{x^{2}−a^{2}} .

(24) Suppose Z ⊆ dom(log (e) · \frac{f_{1}}{f_{2}} ) and for every x such that x ∈ Z holds f_{1}(x) = x − a and f_{1}(x) > 0 and f_{2}(x) = x − b and f_{2}(x) > 0. Then log (e) · \frac{f_{1}}{f_{2}} is differentiable on Z and for every x such that x ∈ Z holds (log (e) · \frac{f_{1}}{f_{2}} )′_{↾Z}(x) = \frac{a−b}{(x−a)·(x−b)}.

(25) Suppose Z ⊆ dom(\frac{1}{a−b} f) and f = log (e) · \frac{f_{1}}{f_{2}} and for every x such that x ∈ Z holds f_{1}(x) = x − a and f_{1}(x) > 0 and f_{2}(x) = x − b and f_{2}(x) > 0 and a − b ≠ 0. Then \frac{1}{a−b} f is differentiable on Z and for every x such that x ∈ Z holds (\frac{1}{a−b} f)′_{↾Z}(x) = \frac{1}{(x−a)·(x−b)}.

(26) Suppose Z ⊆ dom(log (e) · \frac{f_{1}}{f_{2}} ) and f_{2} = _{ℤ}^{2} and for every x such that x ∈ Z holds f_{1}(x) = x − a and f_{1}(x) > 0 and f_{2}(x) > 0 and x ≠ 0. Then log (e) · \frac{f_{1}}{f_{2}} is differentiable on Z and for every x such that x ∈ Z holds (log (e) · \frac{f_{1}}{f_{2}} )′_{↾Z}(x) = \frac{2·a−x}{x·(x−a)}.

(27) Suppose Z ⊆ dom((ℝ^{\frac{3}{2}}) · f) and for every x such that x ∈ Z holds f(x) = a + x and f(x) > 0. Then (ℝ^{\frac{3}{2}}) · f is differentiable on Z and for every x such that x ∈ Z holds ((ℝ^{\frac{3}{2}}) · f)′_{↾Z}(x) = \frac{3}{2} · (a + x)ℝ^{\frac{1}{2}}.

(28) Suppose Z ⊆ dom(\frac{2}{3} ((ℝ^{\frac{3}{2}}) · f)) and for every x such that x ∈ Z holds f(x) = a + x and f(x) > 0. Then \frac{2}{3} ((ℝ^{\frac{3}{2}}) · f) is differentiable on Z and for every x such that x ∈ Z holds (\frac{2}{3} ((ℝ^{\frac{3}{2}}) · f))′_{↾Z}(x) = (a + x)ℝ^{\frac{1}{2}}.

(29) Suppose Z ⊆ dom((−\frac{2}{3}) ((ℝ^{\frac{3}{2}}) · f)) and for every x such that x ∈ Z holds f(x) = a − x and f(x) > 0. Then (−\frac{2}{3}) ((ℝ^{\frac{3}{2}}) · f) is differentiable on Z and for every x such that x ∈ Z holds ((−\frac{2}{3}) ((ℝ^{\frac{3}{2}}) · f))′_{↾Z}(x) = (a − x)ℝ^{\frac{1}{2}}.

(30) Suppose Z ⊆ dom(2 ((ℝ^{\frac{1}{2}}) · f)) and for every x such that x ∈ Z holds f(x) = a + x and f(x) > 0. Then 2 ((ℝ^{\frac{1}{2}}) · f) is differentiable on Z and for every x such that x ∈ Z holds (2 ((ℝ^{\frac{1}{2}}) · f))′_{↾Z}(x) = (a + x)_{ℝ}^{− \frac{1}{2}}.

(31) Suppose Z ⊆ dom((−2) ((ℝ^{\frac{1}{2}}) · f)) and for every x such that x ∈ Z holds f(x) = a − x and f(x) > 0. Then (−2) ((ℝ^{\frac{1}{2}}) · f) is differentiable on Z and for every x such that x ∈ Z holds ((−2) ((ℝ^{\frac{1}{2}}) · f))′_{↾Z}(x) = (a − x)_{ℝ}^{− \frac{1}{2}}.

(32) Suppose Z ⊆ dom(\frac{2}{3·b} ((ℝ^{\frac{3}{2}}) · f)) and for every x such that x ∈ Z holds f(x) = a + b · x and b ≠ 0 and f(x) > 0. Then \frac{2}{3·b} ((ℝ^{\frac{3}{2}}) · f) is differentiable on Z and for every x such that x ∈ Z holds (\frac{2}{3·b} ((ℝ^{\frac{3}{2}})·f))′_{↾Z}(x) = (a+b·x)ℝ^{\frac{1}{2}}.

(33) Suppose Z ⊆ dom((−\frac{2}{3·b}) ((ℝ^{\frac{3}{2}})·f)) and for every x such that x ∈ Z holds f(x) = a−b·x and b ≠ 0 and f(x) > 0. Then (−\frac{2}{3·b}) ((ℝ^{\frac{3}{2}})·f) is differentiable on Z and for every x such that x ∈ Z holds ((−\frac{2}{3·b}) ((ℝ^{\frac{3}{2}}) · f))′_{↾Z}(x) =

(a − b · x)ℝ^{\frac{1}{2}}.

(34) Suppose Z ⊆ dom((ℝ^{\frac{1}{2}})·f) and f = f_{1}+f_{2} and f_{2} = _{ℤ}^{2} and for every x such that x ∈ Z holds f_{1}(x) = a^{2} and f(x) > 0. Then (ℝ^{\frac{1}{2}})·f is differentiable on

Z and for every x such that x ∈ Z holds ((ℝ^{\frac{1}{2}}) · f)′_{↾Z}(x) = x · (a^{2} + x^{2})_{ℝ}^{− \frac{1}{2}}.

(35) Suppose Z ⊆ dom(−(ℝ^{\frac{1}{2}}) · f) and f = f_{1} − f_{2} and f_{2} = _{ℤ}^{2} and for every

x such that x ∈ Z holds f_{1}(x) = a^{2} and f(x) > 0. Then −(ℝ^{\frac{1}{2}}) · f is

differentiable on Z and for every x such that x ∈ Z holds (−(ℝ^{\frac{1}{2}}) · f)′_{↾Z}(x) =

x · (a^{2} − x^{2})_{ℝ}^{− \frac{1}{2}}.

(36) Suppose Z ⊆ dom(2 ((ℝ^{\frac{1}{2}}) · f)) and f = f_{1} + f_{2} and f_{2} = _{ℤ}^{2} and for

every x such that x ∈ Z holds f_{1}(x) = x and f(x) > 0. Then 2 ((ℝ^{\frac{1}{2}}) · f)

is differentiable on Z and for every x such that x ∈ Z holds (2 ((ℝ^{\frac{1}{2}}) ·

f))′_{↾Z}(x) = (2 · x + 1) · (x^{2} + x)_{ℝ}^{− \frac{1}{2}}.

(37) Suppose Z ⊆ dom((the function sin) ·f) and for every x such that x ∈ Z

holds f(x) = a · x + b. Then

(i) (the function sin) ·f is differentiable on Z, and (ii) for every x such that x ∈ Z holds ((the function sin) ·f)′_{↾Z}(x) = a · (the

function cos)(a · x + b).

(38) Suppose Z ⊆ dom((the function cos) ·f) and for every x such that x ∈ Z

holds f(x) = a · x + b. Then

(i) (the function cos) ·f is differentiable on Z, and (ii) for every x such that x ∈ Z holds ((the function cos) ·f)′_{↾Z}(x) =

−a · (the function sin)(a · x + b).

(39) Suppose that for every x such that x ∈ Z holds (the function cos)(x) ≠ 0.

Then

(i) \frac{1}{the function cos} is differentiable on Z, and (ii) for every x such that x ∈ Z holds (\frac{1}{the function cos})′_{↾Z}(x) =

\frac{(the function sin)(x)}{(the function cos)(x)^{2}} .

(40) Suppose that for every x such that x ∈ Z holds (the function sin)(x) ≠ 0.

Then

(i) \frac{1}{the function sin} is differentiable on Z, and (ii) for every x such that x ∈ Z holds (\frac{1}{the function sin})′_{↾Z}(x) =

−\frac{(the function cos)(x)}{(the function sin)(x)^{2}} .

(41) Suppose Z ⊆ dom((the function sin) (the function cos)). Then (i) (the function sin) (the function cos) is differentiable on Z, and (ii) for every x such that x ∈ Z holds ((the function sin) (the function

cos))′_{↾Z}(x) = cos(2 · x).

(42) Suppose Z ⊆ dom(log (e) · (the function cos)) and for every x such that x ∈ Z holds (the function cos)(x) > 0. Then log (e) · (the function cos) is differentiable on Z and for every x such that x ∈ Z holds (log (e) · (the function cos))′_{↾Z}(x) = −tan x.

(43) Suppose Z ⊆ dom(log (e) · (the function sin)) and for every x such that x ∈ Z holds (the function sin)(x) > 0. Then log (e) · (the function sin) is differentiable on Z and for every x such that x ∈ Z holds (log (e) · (the function sin))′_{↾Z}(x) = cot x.

(44) Suppose Z ⊆ dom((−id_{Z}) (the function cos)). Then (i) (−id_{Z}) (the function cos) is differentiable on Z, and (ii) for every x such that x ∈ Z holds ((−id_{Z}) (the function cos))′_{↾Z}(x) =

−(the function cos)(x) + x · (the function sin)(x).

(45) Suppose Z ⊆ dom(id_{Z} (the function sin)). Then (i) id_{Z} (the function sin) is differentiable on Z, and (ii) for every x such that x ∈ Z holds (id_{Z} (the function sin))′_{↾Z}(x) = (the

function sin)(x) + x · (the function cos)(x).

(46) Suppose Z ⊆ dom((−id_{Z}) (the function cos)+the function sin). Then (i) (−id_{Z}) (the function cos)+the function sin is differentiable on Z, and (ii) for every x such that x ∈ Z holds ((−id_{Z}) (the function cos)+the

function sin)′_{↾Z}(x) = x · (the function sin)(x).

(47) Suppose Z ⊆ dom(id_{Z} (the function sin)+the function cos). Then (i) id_{Z} (the function sin)+the function cos is differentiable on Z, and (ii) for every x such that x ∈ Z holds (id_{Z} (the function sin)+the function

cos)′_{↾Z}(x) = x · (the function cos)(x).

(48) Suppose Z ⊆ dom(2 ((ℝ^{\frac{1}{2}}) · (the function sin))) and for every x such that

x ∈ Z holds (the function sin)(x) > 0. Then

(i) 2 ((ℝ^{\frac{1}{2}}) · (the function sin)) is differentiable on Z, and

(ii) for every x such that x ∈ Z holds (2 ((ℝ^{\frac{1}{2}}) · (the function sin)))′_{↾Z}(x) =

(the function cos)(x) · (the function sin)(x)_{ℝ}^{− \frac{1}{2}}.

(49) Suppose Z ⊆ dom(\frac{1}{2} ((_{ℤ}^{2}) · (the function sin))). Then (i) \frac{1}{2} ((_{ℤ}^{2}) · (the function sin)) is differentiable on Z, and (ii) for every x such that x ∈ Z holds (\frac{1}{2} ((_{ℤ}^{2}) · (the function sin)))′_{↾Z}(x) =

(the function sin)(x) · (the function cos)(x).

(50) Suppose that (i) Z ⊆ dom((the function sin)+\frac{1}{2} ((_{ℤ}^{2}) · (the function sin))), and (ii) for every x such that x ∈ Z holds (the function sin)(x) > 0 and (the

function sin)(x) < 1. Then

(iii) (the function sin)+\frac{1}{2} ((_{ℤ}^{2})·(the function sin)) is differentiable on Z, and (iv) for every x such that x ∈ Z holds ((the function sin)+\frac{1}{2} ((_{ℤ}^{2}) · (the

function sin)))′_{↾Z}(x) = \frac{(the function cos)(x)^{3}}{1−(the function sin)(x)}.

(51) Suppose that (i) Z ⊆ dom(\frac{1}{2} ((_{ℤ}^{2}) · (the function sin))−the function cos), and (ii) for every x such that x ∈ Z holds (the function sin)(x) > 0 and (the

function cos)(x) < 1. Then

(iii) \frac{1}{2} ((_{ℤ}^{2}) · (the function sin))−the function cos is differentiable on Z, and (iv) for every x such that x ∈ Z holds (\frac{1}{2} ((_{ℤ}^{2}) · (the function sin))−the

function cos)′_{↾Z}(x) = \frac{(the function sin)(x)^{3}}{1−(the function cos)(x)}.

(52) Suppose that (i) Z ⊆ dom((the function sin)−\frac{1}{2} ((_{ℤ}^{2}) · (the function sin))), and (ii) for every x such that x ∈ Z holds (the function sin)(x) > 0 and (the

function sin)(x) > −1. Then

(iii) (the function sin)−\frac{1}{2} ((_{ℤ}^{2})·(the function sin)) is differentiable on Z, and (iv) for every x such that x ∈ Z holds ((the function sin)−\frac{1}{2} ((_{ℤ}^{2}) · (the

function sin)))′_{↾Z}(x) = \frac{(the function cos)(x)^{3}}{1+(the function sin)(x)}.

(53) Suppose that (i) Z ⊆ dom(−the function cos − \frac{1}{2} ((_{ℤ}^{2}) · (the function sin))), and (ii) for every x such that x ∈ Z holds (the function sin)(x) > 0 and (the

function cos)(x) > −1. Then

(iii) −the function cos − \frac{1}{2} ((_{ℤ}^{2}) · (the function sin)) is differentiable on Z,

and (iv) for every x such that x ∈ Z holds (−the function cos − \frac{1}{2} ((_{ℤ}^{2}) · (the

function sin)))′_{↾Z}(x) = \frac{(the function sin)(x)^{3}}{1+(the function cos)(x)}.

(54) Suppose Z ⊆ dom(\frac{1}{n} ((_{ℤ}^{n}) · (the function sin))) and n > 0. Then (i) \frac{1}{n} ((_{ℤ}^{n}) · (the function sin)) is differentiable on Z, and (ii) for every x such that x ∈ Z holds (\frac{1}{n} ((_{ℤ}^{n}) · (the function sin)))′_{↾Z}(x) =

((the function sin)(x)_{ℤ}^{n−1}) · (the function cos)(x).

(55) Suppose Z ⊆ dom(exp f) and for every x such that x ∈ Z holds f(x) = x − 1. Then exp f is differentiable on Z and for every x such that x ∈ Z holds (exp f)′_{↾Z}(x) = x · exp(x).

(56) Suppose Z ⊆ dom(log (e)· \frac{exp}{exp +f}) and for every x such that x ∈ Z holds f(x) = 1. Then log (e) · \frac{exp}{exp +f} is differentiable on Z and for every x such that x ∈ Z holds (log (e) · \frac{exp}{exp +f})′_{↾Z}(x) = \frac{1}{exp(x)+1}.

(57) Suppose Z ⊆ dom(log (e)· \frac{exp −f}{exp} ) and for every x such that x ∈ Z holds f(x) = 1 and (exp −f)(x) > 0. Then log (e) · \frac{exp −f}{exp} is differentiable on Z and for every x such that x ∈ Z holds (log (e) · \frac{exp −f}{exp} )′_{↾Z}(x) = \frac{1}{exp(x)−1}.

434 yan zhang and xiquan liang

References

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

[2] Pacharapokin Chanapat, Kanchun, and Hiroshi Yamazaki. Formulas and identities of trigonometric functions. Formalized Mathematics, 12(2):139–141, 2004.

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

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

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

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

[7] Konrad Raczkowski. Integer and rational exponents. Formalized Mathematics, 2(1):125– 130, 1991.

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

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

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

[11] Yasunari Shidama. The Taylor expansions. Formalized Mathematics, 12(2):195–200, 2004.

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

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

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

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

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

[17] Yuguang Yang and Yasunari Shidama. Trigonometric functions and existence of circle ratio. Formalized Mathematics, 7(2):255–263, 1998.

Contents Formaliz. Math. 13 (3)

Properties of First and Second Order Cutting of Binary Relations

By Krzysztof Retel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 361

The Inner Product and Conjugate of Finite Sequences of Complex

Numbers

By Wenpai Chang et al. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 367

Inferior Limit and Superior Limit of Sequences of Real Numbers

By Bo Zhang et al. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 375

Formulas and Identities of Inverse Hyperbolic Functions

By Fuguo Ge and Xiquan Liang and Yuzhong Ding . . . . . 383

Lines on Planes in n-Dimensional Euclidean Spaces

By Akihiro Kubo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 389

Cardinal Numbers and Finite Sets

By Karol Pa̧k . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 399

Some Equations Related to the Limit of Sequence of Subsets

By Bo Zhang et al. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 407

On the Partial Product of Series and Related Basic Inequalities

By Fuguo Ge and Xiquan Liang . . . . . . . . . . . . . . . . . . . . . . . . 413

Homeomorphism between Finite Topological Spaces, Two-Dimensional

Lattice Spaces and a Fixed Point Theorem

By Masami Tanaka et al. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 417

The Maclaurin Expansions

By Akira Nishino and Yasunari Shidama . . . . . . . . . . . . . . . 421

Several Differentiable Formulas of Special Functions

By Yan Zhang and Xiquan Liang . . . . . . . . . . . . . . . . . . . . . . . 427

Continued on inside back cover