Lemmas `fiberwise_{finite,countable}_preimage`

[t6s]

Motivation for this change

Add lemmas stating that the preimage of a set along a function is finite / countable if every pointwise preimage is so.

NB: there is already finite_preimage which is similar but for injective preimages.

Checklist

• [x] added corresponding entries in CHANGELOG_UNRELEASED.md

• [ ] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[t6s]

TODO:

1. create a renaming PR : finite_preimage -> finite_inj_preimage
2. redo this PR