Miscellaneous Facts about Functions
Grzegorz Bancerek, Andrzej Trybulec · 1996
We follow the rules: a, x, A, B denote sets and m, n denote natural numbers. The following propositions are true: (1) For every function f and for every set X such that rng f ⊆ X holds idX · f = f. (2) Let X be a set, Y be a non empty set, and f be a function from X into Y. Suppose f is one-to-one. Let B be a subset of X and C be a subset of Y. If C ⊆ f ◦ B, then f −1 (C) ⊆ B. (3) Let X, Y be non empty sets and f be a function from X into Y. Suppose f is one-to-one. Let x be an element of X and A be a subset of X. If f(x) ∈ f ◦ A, then x ∈ A. (4) Let X, Y be non empty sets and f be a function from X into Y. Suppose f is one-to-one. Let x be an element of X, A be a subset of X, and B be a subset of Y. If f(x) ∈ f ◦ A \\ B, then x ∈ A \\ f −1 (B). (5) Let X, Y be non empty sets and f be a function from X into Y. Suppose f is one-to-one. Let y be an element of Y, A be a subset of X, and B be a subset of Y. If y ∈ f ◦ A \\ B, then f −1 (y) ∈ A \\ f −1 (B). (6) For every function f and for every set a such that a ∈ dom f holds f↾{a} = a↦− →. Let x, y be sets. Observe that x↦− →. y is non empty.