English
A finite set of subsets that forms a partition yields a finpartition of Set.univ; the resulting finite partition has prescribed independence and supremum properties.
Русский
Для конечного разбиения \n {c : Finset (Set α)} существует соответствующее конечное разбиение Set.univ с заданными свойствами независимости и объединения.
LaTeX
$$$\\text{finpartition}\\; (hc : \\text{Setoid.IsPartition} (c : Set (Set α))) : \\text{Finpartition}(Set.univ)$$$
Lean4
/-- A finite setoid partition furnishes a finpartition -/
@[simps]
def finpartition {c : Finset (Set α)} (hc : Setoid.IsPartition (c : Set (Set α))) : Finpartition (Set.univ : Set α)
where
parts := c
supIndep := Finset.supIndep_iff_pairwiseDisjoint.mpr <| eqv_classes_disjoint hc.2
sup_parts := c.sup_id_set_eq_sUnion.trans hc.sUnion_eq_univ
bot_notMem := hc.left
