English
In a set semiring C, for all s,t ∈ C, the difference s \ t can be written as a finite disjoint union of sets from C. The finite family is not unique, but a particular one is chosen to satisfy the equality. The empty set is removed to ensure t ∉ disjointOfDiff.
Русский
В полупрямой системе C для всех s,t ∈ C разность s \ t выражается как конечное дисjointное объединение элементов C. Конкретная конечная семейство не уникально, но выбирается такое, чтобы equality выполнялось; пустое множество удаляется, чтобы исключить ситуацию t = ∅.
LaTeX
$$$\exists F \in \mathrm{Finset}(\mathcal{P}(\alpha)),\ (\forall A \in F, A\in C) \wedge (s\setminus t) = \bigcup F \wedge F\text{ разбивает разность на попарно непересекающиеся части}.$$$
Lean4
/-- In a semi-ring of sets `C`, for all sets `s, t ∈ C`, `s \ t` is equal to a disjoint union of
finitely many sets in `C`. The finite set of sets in the union is not unique, but this definition
gives an arbitrary `Finset (Set α)` that satisfies the equality.
We remove the empty set to ensure that `t ∉ hC.disjointOfDiff hs ht` even if `t = ∅`. -/
noncomputable def disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) : Finset (Set α) :=
(hC.diff_eq_sUnion' s hs t ht).choose \ {∅}
