Metamath Proof Explorer


Table of Contents - 21.50.7. Preimages of function values

According to Wikipedia ("Image (mathematics)", 17-Mar-2024, https://en.wikipedia.org/wiki/ImageSupport_(mathematics)): "... evaluating a given function at each element of a given subset of its domain produces a set, called the "image of under (or through) ". Similarly, the inverse image (or preimage) of a given subset of the codomain of is the set of all elements of the domain that map to the members of ." The preimage of a set under a function is often denoted as "f^-1 (B)", but in set.mm, the idiom is used. As a special case, the idiom for the preimage of a function value at under a function is (according to Wikipedia, the preimage of a singleton is also called a "fiber").

We use the label fragment "preima" (as in mptpreima) for theorems about preimages (sometimes, also "imacnv" is used as in fvimacnvi), and "preimafv" (as in preimafvn0) for theorems about preimages of a function value.

In this section, will be the set of all preimages of function values of a function , that means is a preimage of a function value (see, for example, elsetpreimafv): .

With the help of such a set, it is shown that every function can be decomposed into a surjective and an injective function (see fundcmpsurinj) by constructing a surjective function and an injective function so that ( see fundcmpsurinjpreimafv). See also Wikipedia ("Surjective function", 17-Mar-2024, https://en.wikipedia.org/wiki/Surjective_function (section "Composition and decomposition"). This is different from the decomposition of into the surjective function (with for ) and the injective function , ( see fundcmpsurinjimaid), see also Wikipedia ("Bijection, injection and surjection", 17-Mar-2024, https://en.wikipedia.org/wiki/Bijection,_injection_and_surjection (section "Properties").

Finally, it is shown that every function can be decomposed into a surjective, a bijective and an injective function (see fundcmpsurbijinj), by showing that there is a bijection between the set of all preimages of values of a function and the range of the function (see imasetpreimafvbij). From this, both variants of decompositions of a function into a surjective and an injective function can be derived:

Let be a decomposition of a function into a surjective, a bijective and an injective function, then with (an injective function) is a decomposition into a surjective and an injective function corresponding to fundcmpsurinj, and with (a surjective function) is a decomposition into a surjective and an injective function corresponding to fundcmpsurinjimaid.

  1. preimafvsnel
  2. preimafvn0
  3. uniimafveqt
  4. uniimaprimaeqfv
  5. setpreimafvex
  6. elsetpreimafvb
  7. elsetpreimafv
  8. elsetpreimafvssdm
  9. fvelsetpreimafv
  10. preimafvelsetpreimafv
  11. preimafvsspwdm
  12. 0nelsetpreimafv
  13. elsetpreimafvbi
  14. elsetpreimafveqfv
  15. eqfvelsetpreimafv
  16. elsetpreimafvrab
  17. imaelsetpreimafv
  18. uniimaelsetpreimafv
  19. elsetpreimafveq
  20. fundcmpsurinjlem1
  21. fundcmpsurinjlem2
  22. fundcmpsurinjlem3
  23. imasetpreimafvbijlemf
  24. imasetpreimafvbijlemfv
  25. imasetpreimafvbijlemfv1
  26. imasetpreimafvbijlemf1
  27. imasetpreimafvbijlemfo
  28. imasetpreimafvbij
  29. fundcmpsurbijinjpreimafv
  30. fundcmpsurinjpreimafv
  31. fundcmpsurinj
  32. fundcmpsurbijinj
  33. fundcmpsurinjimaid
  34. fundcmpsurinjALT