Partition

• Partition #Card
  • A family $\mathcal{A}$ of subsets of $X$ is a partition if $A_0 \cap A_1 = \emptyset$ whenever $A_0 \neq A_1$, and $\bigcup \mathcal{A} = X$.

Back

A family $\mathcal{A}$ of subsets of $X$ is a partition if $A_0 \cap A_1 = \emptyset$ whenever $A_0 \neq A_1$, and $\bigcup \mathcal{A} = X$.

Lean

Setoid.IsPartition / Setoid.classes