Hi gang,
Given a set S, of records where each record has a field f such that \A s \in S: s[f] \in Nat, I am trying to prove the following lemma:
IsFiniteSet(S) => IsFiniteSet({s.f: s \in S})
As far as I could tell, there is no direct theorem in FiniteSetTheorems which can discharge this. There however are other ways. Some of them are:
1) Prove that {s.f: s \in S} can be obtained from a surjection on S and then use FS_Surjection.
2) Prove that \A s \in S : IsFiniteSet({s.f}) using FS_Singleton and then use FS_UNION to prove {{s.f}: s \in S} is finite. But I think here the above surjection would still be needed.
3) Write an inductive proof on S.
I was wondering if others have tried to prove something along the lines of this before (collection of elements of finite sets of records), and how have others tried to prove it.
Thanks,
Saksham Chand
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to
tla...@xxxxxxxxxxxxxxxx.
Visit this group at
https://groups.google.com/group/tlaplus.
For more options, visit
https://groups.google.com/d/optout.