English
A collection c of subsets of α is a partition of α into pairwise disjoint nonempty sets if ∅ ∉ c and every a ∈ α lies in a unique b ∈ c.
Русский
Коллекция c подмножеств α образует разбиение α на попарно непересекающиеся непустые множества, если ∅ не принадлежит c и каждый элемент a ∈ α принадлежит ровно одному множеству b ∈ c.
LaTeX
$$$\\\\emptyset \\\\notin c \\\\wedge \\\\forall a, \\\\exists! b \\\\in c, a \\\\in b$$$
Lean4
/-- A collection `c : Set (Set α)` of sets is a partition of `α` into pairwise
disjoint sets if `∅ ∉ c` and each element `a : α` belongs to a unique set `b ∈ c`. -/
def IsPartition (c : Set (Set α)) :=
∅ ∉ c ∧ ∀ a, ∃! b ∈ c, a ∈ b
