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

*From*: saksha...@xxxxxxxxxxxxxx*Date*: Mon, 27 Mar 2017 07:32:20 -0700 (PDT)

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

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

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

- Prev by Date:
**Re: [tlaplus] Fatal error starting 1.5.2 on macOS Sierra, and a solution.** - Next by Date:
**Re: [tlaplus] About Finite Set of records** - Previous by thread:
**Re: [tlaplus] Fatal error starting 1.5.2 on macOS Sierra, and a solution.** - Next by thread:
**Re: [tlaplus] About Finite Set of records** - Index(es):