# [tlaplus] library of simple finite set properties?

• From: "David N. Jansen" <dnjansen@xxxxxxxxx>
• Date: Thu, 21 Mar 2019 04:00:27 +0000
• Accept-language: nl-NL, zh-CN, en-US
• Thread-topic: library of simple finite set properties?

Dear all,

I would like to get proofs of a few simple lemmas about IsFiniteSet and Cardinality, properties like:

\A S, T: IsFiniteSet(S) /\ IsFiniteSet(T) => IsFiniteSet(S \union T)

\A S: IsFiniteSet(S) => Cardinality(S) \in Nat
\A S, T: IsFiniteSet(S) /\ IsFiniteSet(T) => Cardinality(S) <= Cardinality(T)
\A i, j \in Int: Cardinality(i .. j) = IF i > j THEN 0 ELSE j - i

I guess that someone has already proofs of these and similar properties and I don't need to redo them. I want to use them to prove correctness of an algorithm and don't want to reinvent mathematics; and while I am ok to leave some of such simple lemmas unproven, I still prefer having a proof if it already exists.

Can someone of you help me? Thank you.

Kind regards,
David N. Jansen.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.