Theorems · Definition · order theory
IndexedPartition.setoid
{ι : Type u_1} → {α : Type u_2} → {s : ι → Set α} → IndexedPartition s → Setoid αThe equivalence relation associated to an indexed partition. Two elements are equivalent if they belong to the same set of the partition.
- Defined in
- Mathlib.Data.Setoid.Partition
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Setoid.kerproof · cited by 43
- IndexedPartitionstatement and proof · cited by 33
- IndexedPartition.indexproof · cited by 22
Cited by4
Results whose statement or proof uses this declaration.
- IndexedPartition.Quotientproof · cited by 9
- IndexedPartition.some_indexstatement · cited by 3
- IndexedPartition.index_outstatement · cited by 0
- IndexedPartition.class_ofstatement · cited by 0