Properties of Real Functions
Jaros law Kotowicz · 2004
The papers [11], [3], [1], [9], [5], [6], [4], [2], [7], [10], and [8] provide the terminology and notation for this paper. For simplicity we follow a convention: x is arbitrary, X, X1, Y denote sets, g, r, r1, r2, p denote real numbers, R denotes a subset of , seq, seq1, seq2, seq3 denote sequences of real numbers, Ns denotes an increasing sequence of naturals, n denotes a natural number, and h, h1, h2 denote partial functions from to . The following propositions are true: (1) For all functions F , G and for every X such that X ⊆ domF and F ◦ X ⊆ domG holds X ⊆ dom(G · F ). (2) For all functions F , G and for every X holds G (F ◦ X) · F X = (G · F ) X. (3) For all functions F , G and for all X, X1 holds G X1 ·F X = (G·F ) (X ∩ F −1 X1). (4) For all functions F , G and for every X holds X ⊆ dom(G · F ) if and only if X ⊆ domF and F ◦ X ⊆ domG. (5) For every function F and for every X holds (F X) ◦ X = F ◦ X. Let us consider seq. Then rng seq is a subset of . One can prove the following propositions: (6) seq1 = seq2 − seq3 if and only if for every n holds seq1(n) = seq2(n)− seq3(n). (7) rng(seq n) ⊆ rng seq.