isPartition_parts — Mathlib

English

A Finpartition gives rise to a setoid partition: the parts form a partition via the induced equivalence relation.

Русский

Finpartition порождает класс разбиений: части образуют разбиение через соответствующее отношение эквивалентности.

LaTeX

$$$\\text{Setoid.IsPartition } (f.parts)$$$

Lean4

/-- A finpartition gives rise to a setoid partition -/
theorem isPartition_parts {α} (f : Finpartition (Set.univ : Set α)) : Setoid.IsPartition (f.parts : Set (Set α)) :=
  ⟨f.bot_notMem,
    Setoid.eqv_classes_of_disjoint_union (f.parts.sup_id_set_eq_sUnion.symm.trans f.sup_parts)
      f.supIndep.pairwiseDisjoint⟩

Похожие утверждения