# Equivalence of Definitions of Semiring of Sets

This page has been identified as a candidate for refactoring.Reshape into standard equivalence proof styleUntil this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |

## Theorem

The following definitions of the concept of **Semiring of Sets** are equivalent:

A collection $\SS$ of subsets of a set $X$ is a semiring (of sets) if and only if:

- $(1): \quad \O \in \SS$
- $(2): \quad A, B \in \SS \implies A \cap B \in \SS$; that is, $\SS$ is $\cap$-stable
- $(3): \quad$ If $A, A_1 \in \SS$ such that $A_1 \subseteq A$, then there exists a finite sequence $A_2, A_3, \ldots, A_n \in \SS$ such that:
- $(3 \text a): \quad \ds A = \bigcup_{k \mathop = 1}^n A_k$
- $(3 \text b): \quad$ The $A_k$ are pairwise disjoint

We prove that criterion $(3)$ can be replaced by:

- $(3'):\quad$ If $A, B \in \SS$, then there exist finite sequence of pairwise disjoint sets $A_1, A_2, \ldots, A_n \in \SS$ such that $\ds A \setminus B = \bigcup_{k \mathop = 1}^n A_k$.

## Proof

### $(3)$ implies $(3')$

Let $X$ be a set, and let $\SS$ be a collection of subsets of $X$.

Suppose that for all $A, A_1 \in \SS$ such that $A_1 \subseteq A$, there exists a finite sequence of sets $A_2, A_3, \ldots, A_n \in \SS$ such that:

- $A_1, A_2, \ldots, A_n$ are pairwise disjoint
- $\ds A = \bigcup_{k \mathop = 1}^n A_k$

Let $B \in \SS$, and let $A_1 = A \cap B$.

It follows that $A_1 \in \SS$, by definition.

Also, $A_1 \subseteq A$ by Intersection is Subset.

Then:

\(\ds A \setminus B\) | \(=\) | \(\ds A \setminus \paren {A \cap B}\) | Set Difference with Intersection is Difference | |||||||||||

\(\ds \) | \(=\) | \(\ds A \setminus A_1\) | ||||||||||||

\(\ds \) | \(=\) | \(\ds \paren {\bigcup_{k \mathop = 1}^n A_k} \setminus A_1\) | ||||||||||||

\(\ds \) | \(=\) | \(\ds \bigcup_{k \mathop = 1}^n \paren {A_k \setminus A_1}\) | Set Difference is Right Distributive over Union | |||||||||||

\(\ds \) | \(=\) | \(\ds \bigcup_{k \mathop = 2}^n \paren {A_k \setminus A_1}\) | Set Difference with Self is Empty Set and Union with Empty Set | |||||||||||

\(\ds \) | \(=\) | \(\ds \bigcup_{k \mathop = 2}^n A_k\) | Set Difference with Disjoint Set |

as required.

$\Box$

### $(3')$ implies $(3)$

Now suppose that for all $A, B \in \SS$, there exists a finite sequence of pairwise disjoint sets $A_1, A_2, \ldots, A_n \in \SS$ such that $\ds A \setminus B = \bigcup_{k \mathop = 1}^n A_k$.

Then $B$ is disjoint with each of the sets $A_k$.

Let $B \subseteq A$. Then:

\(\ds B \cup \bigcup_{k \mathop = 1}^n A_k\) | \(=\) | \(\ds \paren {A \setminus B} \cup B\) | ||||||||||||

\(\ds \) | \(=\) | \(\ds A \cup B\) | Set Difference Union Second Set is Union | |||||||||||

\(\ds \) | \(=\) | \(\ds A\) | Union with Superset is Superset |

as required.

$\blacksquare$