Theorems · Definition · order theory
Setoid.IsPartition
{α : Type u_1} → Set (Set α) → PropA 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.
- Defined in
- Mathlib.Data.Setoid.Partition
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- ExistsUniqueproof · cited by 268
Cited by27
Results whose statement or proof uses this declaration.
- Set.PairwiseDisjoint.isPartition_of_exists_of_ne_emptystatement · cited by 2
- MulAction.IsBlockSystemproof · cited by 2
- AddAction.IsBlockSystemproof · cited by 2
- Setoid.IsPartition.ncard_eq_finsumstatement and proof · cited by 2
- SimpleGraph.Partition.isPartitionstatement · cited by 2
- Setoid.Partitionsproof · cited by 2
- MulAction.IsPartition.of_orbitsstatement · cited by 1
- Setoid.exists_of_mem_partitionstatement and proof · cited by 1
- Setoid.isPartition_classesstatement · cited by 1
- Setoid.IsPartition.finpartitionstatement and proof · cited by 1
- Setoid.nonempty_of_mem_partitionstatement and proof · cited by 1
- SimpleGraph.Partition.mk.injstatement and proof · cited by 1