Grace/Cumulus/Cardinal/InclusionExclusion.g17

Open in Workbench Download source

Imports

NaturalSum · Pigeonhole

Declarations

• cardinality.inclusion_exclusion theorem derivation

Source

1-- Inclusion–exclusion for two finite sets: the sizes of the union and the2-- intersection add up to the sizes of the two sets.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Cardinal.InclusionExclusion9import NaturalSum10import Pigeonhole1112theorem cardinality.inclusion_exclusion (A B : Set)13  requires finiteA : Finite(A)14  requires finiteB : Finite(B)15  shows cardinality(A ∪ B) + cardinality(A ∩ B) =16    cardinality(A) + cardinality(B)17proof18  have restSubset := difference.subset_left at B, A with *19  have finiteRest := Finite.subset with finiteB, restSubset20  have meetSubset := intersection.subset_left at A, B with *21  have finiteMeet := Finite.subset with finiteA, meetSubset22  have splitUnion := difference.union2_self at A, B with *23  have disjointRest : Disjoint(A, B ∖ A)24    unfold Disjoint25    ext x26    simp27  have unionCount := cardinality.union_disjoint with28    finiteA, finiteRest, disjointRest29  rw splitUnion at unionCount30  have splitB : (A ∩ B) ∪ (B ∖ A) = B31    ext x32    simp33  have disjointMeet : Disjoint(A ∩ B, B ∖ A)34    unfold Disjoint35    ext x36    simp37  have meetCount := cardinality.union_disjoint with38    finiteMeet, finiteRest, disjointMeet39  rw splitB at meetCount40  have natA := cardinality.nat with finiteA41  have natMeet := cardinality.nat with finiteMeet42  have natRest := cardinality.nat with finiteRest43  have regroup := add.associative at cardinality(B ∖ A), cardinality(A ∩ B),44    cardinality(A) with natA45  have swap := add.commutative at cardinality(A ∩ B), cardinality(B ∖ A)46    with natMeet, natRest47  rw [unionCount, meetCount, regroup, swap]48  rfl49