[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: saksha...@xxxxxxxxxxxxxx*Date*: Mon, 27 Mar 2017 08:43:31 -0700 (PDT)*References*: <bd841595-1047-4a88-9630-3c78a71dc53a@googlegroups.com> <E239B6E0-3390-430B-9F99-E17A70481320@gmail.com>

Thanks Stephan! That's exactly what I'd written.

On Monday, March 27, 2017 at 10:44:13 AM UTC-4, Stephan Merz wrote:

On Monday, March 27, 2017 at 10:44:13 AM UTC-4, Stephan Merz wrote:

Hi Saksham,thanks for asking – here is your proof (I'm assuming that your module EXTENDs FiniteSetTheorems, included in the distribution of TLAPS).LEMMAASSUME NEW S, IsFiniteSet(S)PROVE IsFiniteSet({s.f: s \in S})<1>. DEFINE T == {s.f: s \in S}proj == [s \in S |-> s.f]<1>. proj \in Surjection(S,T) BY DEF Surjection<1>. QED BY FS_SurjectionCheers,StephanOn 27 Mar 2017, at 16:32, saks...@xxxxxxxxxxxxxx wrote: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...@googlegroups.com .

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 .

**References**:**About Finite Set of records***From:*saksha . . .

**Re: [tlaplus] About Finite Set of records***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] About Finite Set of records** - Next by Date:
**Re: [tlaplus] Next release?** - Previous by thread:
**Re: [tlaplus] About Finite Set of records** - Next by thread:
**Unfolding macro definitions** - Index(es):