TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-06 (claude-opus-5)

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.

Let $\sim$ be an equivalence relation on $A$ with quotient map $\pi : A \to A/{\sim}$ , and let $f : A \to B$ . There is a function $g : A/{\sim} \to B$ with $g \circ \pi = f$ if and only if $a \sim a'$ implies $f(a) = f(a')$ ; and such a $g$ is then unique

Statement

Let $\sim$ be an equivalence relation on a set $A$ , let $A/{\sim}$ be its quotient set and let $\pi := \{\,(a,C) \in A \times (A/{\sim}) : C = [a]\,\}$ , the quotient map. Let $f : A \to B$ . Then $\pi$ is a surjective function $A \to A/{\sim}$ with $\pi(a) = [a]$ , and:

(i) there is a function $g : A/{\sim} \to B$ with $g \circ \pi = f$ if and only if $f(a) = f(a')$ whenever $a \sim a'$ ;
(ii) when such a $g$ exists it is unique, and it satisfies $g([a]) = f(a)$ for every $a \in A$ .

Facts & Assumptions

Given: an equivalence relation $\sim$ on a set $A$ and a function $f : A \to B$ .

[L1]

reflexive: $a \sim a$ for every $a \in A$ (Equivalence relation, equivalence class, and the quotient set $A/{\sim}$ ).

[L2]

symmetric: $a \sim b$ implies $b \sim a$ , for all $a, b \in A$ (Equivalence relation, equivalence class, and the quotient set $A/{\sim}$ ).

[L3]

transitive: $a \sim b$ and $b \sim c$ imply $a \sim c$ , for all $a, b, c \in A$ (Equivalence relation, equivalence class, and the quotient set $A/{\sim}$ ).

[L4]

$[a] \;:=\; \{\, b \in A \;:\; a \sim b \,\} \;\subseteq\; A$ (Equivalence relation, equivalence class, and the quotient set $A/{\sim}$ ).

[L5]

$A/{\sim} \;:=\; \{\, [a] \;:\; a \in A \,\}$ (Equivalence relation, equivalence class, and the quotient set $A/{\sim}$ ).

[L6]

We write $f : A \to B$ , and say $f$ is a function from $A$ to $B$ , when $f$ is a function with $\operatorname{dom} f = A$ and $\operatorname{ran} f \subseteq B$ (A function is a relation $f$ with $(a,b) \in f$ and $(a,c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f(a)$ , domain and codomain).

[L7]

$f = g$ if and only if $\operatorname{dom} f = \operatorname{dom} g$ and $f(x) = g(x)$ for every $x \in \operatorname{dom} f$ (Functions $f$ and $g$ are equal if and only if $\operatorname{dom} f = \operatorname{dom} g$ and $f(x) = g(x)$ for every $x$ in that common domain).

[L8]

$f$ is surjective (onto) if for every $b \in B$ there is some $x \in A$ with $f(x) = b$ (Injection, surjection, bijection).

[L9]

$z \in A \times B$ holds if and only if $z = (a,b)$ for some $a \in A$ and some $b \in B$ (The Cartesian product $A \times B := \{\, z \in \mathcal{P}(\mathcal{P}(A \cup B)) : \exists a \in A\ \exists b \in B\ z = (a,b) \,\}$ ).

[L10]

For any parameters $\bar p$ and any set $x$ , there is a set $y$ whose elements are exactly the elements $z$ of $x$ for which $\varphi(z,\bar p)$ holds (The Axiom Schema of Separation: for each formula $\varphi$ , $\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p)))$ ).

[L11]

$g \circ f$ is a function, $\operatorname{dom}(g \circ f) = f^{-1}[\operatorname{dom} g]$ , and $(g \circ f)(x) = g(f(x))$ for every $x$ in that domain (If $f$ and $g$ are functions then $g \circ f$ is a function with domain $f^{-1}[\operatorname{dom} g]$ and $(g \circ f)(x) = g(f(x))$ there; $\Delta_A$ is a function with $\Delta_A(a) = a$ ; and $f \circ \Delta_A = f = \Delta_B \circ f$ for $f : A \to B$ ).

[L12]

$\operatorname{dom} R := \{\, a : \exists b\ (a,b) \in R \,\}, \qquad \operatorname{ran} R := \{\, b : \exists a\ (a,b) \in R \,\}$ (Relation, $\operatorname{dom} R$ , $\operatorname{ran} R$ , $\operatorname{fld} R$ , and the specialisations "relation from $A$ to $B$ " and "relation on $A$ ").

[L13]

$z \in \mathcal{P}(x)$ holds if and only if $z \subseteq x$ (The power set $\mathcal{P}(x) = \{\, z : z \subseteq x \,\}$ ).

[L14]

$x \subseteq y$ means that every element of $x$ is an element of $y$ (Subset $x \subseteq y$ , proper subset $x \subsetneq y$ , and the separation notation $\{\, z \in x : \varphi(z) \,\}$ ).

Proof

technique · direct

1.1

$[a] = [a']$ holds if and only if $a \sim a'$ . If $a \sim a'$ , then for $b \in A$ we get $b \in [a]$ exactly when $a \sim b$ , and symmetry with transitivity turns that into $a' \sim b$ , so $[a] \subseteq [a']$ ; the same argument with $a$ and $a'$ exchanged gives the reverse inclusion. Conversely $a \in [a]$ by reflexivity, so $[a] = [a']$ gives $a \in [a']$ , that is $a' \sim a$ , and symmetry gives $a \sim a'$ .

L1L2L3L4L14

1.2

$\pi$ is a surjective function $A \to A/{\sim}$ with $\pi(a) = [a]$ : it is a set by separation inside $A \times (A/{\sim})$ , it is single valued because $[a]$ is determined by $a$ , its domain is $A$ since $[a] \in A/{\sim}$ for every $a \in A$ , and every element of $A/{\sim}$ is $[a]$ for some $a \in A$ , so it is onto.

L4L5L6L8L9L10L12

1.3

Uniqueness in (ii): if $g$ and $g'$ are functions $A/{\sim} \to B$ with $g \circ \pi = f = g' \circ \pi$ , then for $C \in A/{\sim}$ choose $a \in A$ with $C = [a]$ ; then $g(C) = g(\pi(a)) = f(a) = g'(\pi(a)) = g'(C)$ . Both have domain $A/{\sim}$ , so $g = g'$ .

L5L6L7L11

2.1

Claim (i), from left to right: suppose $g : A/{\sim} \to B$ satisfies $g \circ \pi = f$ , and let $a \sim a'$ . Then $[a] = [a']$ , so $f(a) = g(\pi(a)) = g([a]) = g([a']) = g(\pi(a')) = f(a')$ .

L11step 1.1step 1.2

2.2

Claim (i), from right to left: suppose $f(a) = f(a')$ whenever $a \sim a'$ , and separate inside $(A/{\sim}) \times B$ to obtain $g := \{\,(C,y) \in (A/{\sim}) \times B : \exists a\,(a \in A \wedge C = [a] \wedge y = f(a))\,\}$ . It is single valued: if $C = [a] = [a']$ with values $f(a)$ and $f(a')$ , then $a \sim a'$ and the hypothesis gives $f(a) = f(a')$ . Its domain is $A/{\sim}$ , since every class is some $[a]$ and then $(C,f(a)) \in g$ , and its range lies in $B$ ; so $g : A/{\sim} \to B$ with $g([a]) = f(a)$ . Finally $g \circ \pi$ and $f$ are functions with domain $A$ and $(g \circ \pi)(a) = g([a]) = f(a)$ , so $g \circ \pi = f$ .

L5L6L7L9L10L11L12L13step 1.1step 1.2

3.1

Both directions of (i) hold, and step 1.3 supplies the uniqueness in (ii) while step 2.2 supplies the formula $g([a]) = f(a)$ , which is the statement.

step 1.1step 1.2step 1.3step 2.1step 2.2∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 31 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Equivalence relation (Wikipedia) (standard reference, not scraped)
Quotient set (Wikipedia) (standard reference, not scraped)
B. Kaya, MATH 320 Set Theory (METU), §3.2 (standard reference, not scraped)