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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 26 Apr 2024 06:37:10 +0200*References*: <07aaecb6-6368-4ffb-b7ca-5579d656a625n@googlegroups.com> <882fb42f-40d7-4ad4-980e-a23a55261fddn@googlegroups.com> <28c9fe31-7a26-428f-af36-4d30c2a618aen@googlegroups.com> <F38F1FE8-B042-445F-875E-99033895FDF2@lemmster.de> <f2c82e65-92e1-4c06-b61a-dfd78d19a017n@googlegroups.com>

As Markus pointed out, cardinality of finite sets is defined in a standard module of TLA+. A collection of lemmas about finite sets and cardinality, useful for actually reasoning about these notions, is available at https://github.com/tlaplus/tlapm/blob/main/library/FiniteSetTheorems.tla (included in the distribution of TLAPS). Stephan
--
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/716A2450-2F69-4E48-98ED-699794A62A69%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Defining Cardinality with TLA***From:*Stephan Merz

**References**:**[tlaplus] Defining Cardinality with TLA***From:*marta zhango

**[tlaplus] Re: Defining Cardinality with TLA***From:*marta zhango

**[tlaplus] Re: Defining Cardinality with TLA***From:*marta zhango

**Re: [tlaplus] Defining Cardinality with TLA***From:*Markus Kuppe

**Re: [tlaplus] Defining Cardinality with TLA***From:*marta zhango

- Prev by Date:
**Re: [tlaplus] TLA and TLAPIS** - Next by Date:
**Re: [tlaplus] Defining Cardinality with TLA** - Previous by thread:
**Re: [tlaplus] Defining Cardinality with TLA** - Next by thread:
**Re: [tlaplus] Defining Cardinality with TLA** - Index(es):