Mathlib Map

Theorems · Definition · order theory

Setoid.classes

{α : Type u_1} → Setoid α → Set (Set α)

Makes the equivalence classes of an equivalence relation.

Defined in
Mathlib.Data.Setoid.Partition
Cited by
17 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SimpleGraph.Coloring.colorClasses · cited by 6Coloring.colorClassesSetoid.mem_classes · cited by 3Setoid.mem_classesSetoid.classes_eqv_classes · cited by 3Setoid.classes_eqv_classesSetoid.classes_ker_subset_fiber_set · cited by 2Setoid.classes_ker_subset…DiscreteQuotient.comp_finsetClopens · cited by 1DiscreteQuotient.comp_fin…SimpleGraph.Coloring.card_colorClasses_le · cited by 1Coloring.card_colorClasse…Setoid.empty_notMem_classes · cited by 1Setoid.empty_notMem_class…Setoid.eq_of_mem_classes · cited by 1Setoid.eq_of_mem_classesSetoid.quotientEquivClasses · cited by 1Setoid.quotientEquivClass…Setoid.finite_classes_ker · cited by 1Setoid.finite_classes_kerSetoid.isPartition_classes · cited by 1Setoid.isPartition_classesSetoid.card_classes_ker_le · cited by 1Setoid.card_classes_ker_leSetoid.classes_inj · cited by 1Setoid.classes_injSetoid.mkClasses_classes · cited by 0Setoid.mkClasses_classesDiscreteQuotient.finsetClopens_inj · cited by 0DiscreteQuotient.finsetCl…Set · cited by 53352SetSet.ofPred · cited by 6101Set.ofPredSetoid.classesCITED BYCITES

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
  • Set.ofPredproof · cited by 6,101

Cited by20

Results whose statement or proof uses this declaration.