Simple Cardinality Proof

So I'm trying to perform a simple proof using cardinalities. It looks like:

⟦(A::nat set) ∩ B = {}⟧ ⟹ (card (A ∪ B) = card A + card B)

Which seems to makes sense, but for some reason blast hangs, the rest of the provers fail to apply, and sledgehammer times out. Is there a gap in what I think I know about cardinalities? If not, how can I prove this lemma?

Thanks in advance!



Read more here: https://stackoverflow.com/questions/67929898/simple-cardinality-proof

Content Attribution

This content was originally published by Kookie at Recent Questions - Stack Overflow, and is syndicated here via their RSS feed. You can read the original post over there.

%d bloggers like this: