How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Equivalence relation, equivalence class, and the quotient set
Definition
A binary relation on a set is a subset (Relation, , , , and the specialisations "relation from to " and "relation on ", The Cartesian product ); we write for and read it " is related to ".
A binary relation on is an equivalence relation when it is reflexive on , symmetric and transitive (Reflexive, irreflexive, symmetric, asymmetric, antisymmetric, transitive, and connex relations on a set), that is, when it is
- reflexive: for every ;
- symmetric: implies , for all ;
- transitive: and imply , for all .
Let be an equivalence relation on . For , the equivalence class of is the subset
and any with is called a representative of the class . The quotient set is the set of all classes,
a subset of the power set of (The power set ). The map (A function is a relation with and implying ; , the value , domain and codomain) with is the quotient map; it is surjective by construction (Injection, surjection, bijection).
Remarks
-
What the classes look like is the content of The equivalence classes of an equivalence relation are nonempty, cover , and are pairwise equal or disjoint; conversely every such cover arises from exactly one equivalence relation: they are nonempty, they cover , and any two of them are either equal or disjoint. That lemma also runs the converse, so "equivalence relation on " and "partition of " are two names for the same data.
-
Well-definedness. A rule that assigns a value to by a formula in the representative defines a function on only if the value is the same for every representative, that is, only if implies that the formula returns the same value at and at . The general statement of that obligation, with the uniqueness of the induced function, is Let be an equivalence relation on with quotient map , and let . There is a function with if and only if implies ; and such a is then unique. The constructions of and of discharge it for their own operations (Integer addition and negation are well defined ↗, Integer multiplication is well defined ↗, Rational arithmetic is well defined ↗).
-
Where the general notion is used. The construction of verifies the three properties for the concrete relation (The integer-defining relation is an equivalence relation ↗), and the construction of does the same for its own relation (The rational-defining relation is an equivalence relation ↗). Each of those items settles one relation and defines no general notion. Cosets, quotient groups, congruence classes and quotient rings are further instances of the definition given here.
Depends on
Relation, , , , and the specialisations "relation from to " and "relation on "
The Cartesian product
Reflexive, irreflexive, symmetric, asymmetric, antisymmetric, transitive, and connex relations on a set
The power set
A function is a relation with and implying ; , the value , domain and codomain
The Axiom Schema of Separation: for each formula ,
Injection, surjection, bijection