English
From a partition c of α into pairwise disjoint sets whose union is α, form the Setoid on α by mkClasses with the equivalence relation determined by eqv_classes_of_disjoint_union.
Русский
Из разбиения c α на пары непересекающихся множеств, чьё объединение равно α, образуется множество эквивалентности на α через mkClasses, используя eqv_classes_of_disjoint_union.
LaTeX
$$$\\text{setoidOfDisjointUnion}(c, hu, H) = \\mathrm{Setoid}.mkClasses\\, c\\, (eqv_classes_of_disjoint_union\\, hu\\, H).$$$
Lean4
/-- Makes an equivalence relation from a set of disjoints sets covering α. -/
def setoidOfDisjointUnion {c : Set (Set α)} (hu : Set.sUnion c = @Set.univ α) (H : c.PairwiseDisjoint id) : Setoid α :=
Setoid.mkClasses c <| eqv_classes_of_disjoint_union hu H
