add pred_infinite_surj

I wondered when pred_infinite (P ∘ f) holds. This is the best lemma I could come up with so far. It's not the lemma I hoped for, but I realized the lemma I hoped for is wrong.^^ However, now that I did this proof, I figured it'd be a waste to throw it away.

added 1 commit

• 996a098d - add pred_infinite_surj

Compare with previous version

Do we also have something like pred_infinite (P ∘ f) → pred_infinite P in case f is injective?

If so, does that property follow from yours, or vice versa?

What kind of a property do we have for pred_finite?

FWIW, the fact that this is in sets.v is rather confusing. We also have infinite.v but that is about a totally different notion of infinity (namely, infinity of a type).

added 1 commit

• 5728445c - generalize to two different types

Compare with previous version

resolved all threads

merged

mentioned in commit bcebd707

mentioned in merge request !238 (merged)