Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Inclusion-exclusion principle in Isabelle?

view this post on Zulip Email Gateway (May 04 2022 at 15:54):

From: Angeliki Koutsoukou Argyraki <ak2110@cam.ac.uk>
Hi,

Do we already have the inclusion-exclusion principle available someplace?
I need to use it for a combinatorics development.

Thank you in advance! Angeliki

view this post on Zulip Email Gateway (May 04 2022 at 16:28):

From: Manuel Eberl <manuel@pruvisto.org>
Yes, it's called card_UNION and it's part of the standard library.

lemma card_UNION:
  assumes "finite A"
    and "∀k ∈ A. finite k"
  shows "card (⋃A) = nat (∑I | I ⊆ A ∧ I ≠ {}. (- 1) ^ (card I + 1) *
int (card (⋂I)))"

Cheers,

Manuel

Last updated: Feb 05 2025 at 16:23 UTC