ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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.

A two-cell partition of a three-element set, the equivalence relation it induces listed pair by pair, and the quotient set recovered from it

Example

Write $u : = \emptyset$ , $v : = {\emptyset}$ and $w : = {\emptyset, {\emptyset}}$ , which are pairwise distinct, and put $A : = {u, v} \cup {w}$ . The collection ${{u, v}, {w}}$ has nonempty cells, covers $A$ , and its two cells are disjoint. The equivalence relation it induces on $A$ , namely " $a$ and $b$ lie in the same cell", is

$\sim = {(u, u), (u, v)} \cup {(v, u), (v, v)} \cup {(w, w)},$

with classes $[u] = [v] = {u, v}$ and $[w] = {w}$ , so that $A / \sim = {{u, v}, {w}}$ is the original collection again.

Facts & Assumptions

Given: $u : = \emptyset$ , $v : = {\emptyset}$ , $w : = {\emptyset, {\emptyset}}$ , $A : = {u, v} \cup {w}$ , and $\sim$ as displayed.

[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]

The equivalence classes of an equivalence relation are nonempty, cover $A$ , and are pairwise equal or disjoint (The equivalence classes of an equivalence relation are nonempty, cover $A$ , and are pairwise equal or disjoint; conversely every such cover arises from exactly one equivalence relation).

[L7]

${x, y}$ is the set whose elements are exactly $x$ and $y$ , and ${x} : = {x, x}$ (The unordered pair ${x, y}$ and the singleton ${x} = {x, x}$ ).

[L8]

There is exactly one set with no elements, written $\emptyset$ (There is exactly one set with no elements, written $\emptyset$ ).

[L9]

$z \in a \cup b$ holds if and only if $z \in a$ or $z \in b$ ( $⋃ \emptyset = \emptyset$ , $⋃ {a} = a$ , $⋃ {a, b} = a \cup b$ , $⋂ {a} = a$ , and $⋂ {a, b} = a \cap b$ ).

[L10]

$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 P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ ).

[L11]

$(a, b) = (c, d)$ if and only if $a = c$ and $b = d$ ( $(a, b) = (c, d)$ if and only if $a = c$ and $b = d$ ).

[L12]

$(a, b) : = {{a}, {a, b}}$ (The Kuratowski ordered pair $(a, b) : = {{a}, {a, b}}$ ).

[L13]

If every $z$ satisfies $z \in x$ if and only if $z \in y$ , then $x = y$ (The Axiom of Extensionality: $\forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \to x = y)$ ).

[L14]

A relation is a set $R$ every element of which is an ordered pair (Relation, $dom R$ , $ran R$ , $fld R$ , and the specialisations "relation from $A$ to $B$ " and "relation on $A$ ").

[L15]

$a \cup b : = ⋃ {a, b}$ (The union $⋃ x$ of a set, and the binary union $a \cup b : = ⋃ {a, b}$ ).

Verification

technique · direct

1.1

$u$ , $v$ and $w$ are pairwise distinct: $u$ has no element, $v$ has exactly $u$ , and $w$ has $v$ as an element while $v$ does not. So $A$ has exactly those three elements, and $\sim$ is a relation on $A$ , each of its five listed pairs having both coordinates in $A$ .

L7L8L9L10L12L14L15

2.1

$\sim$ is an equivalence relation on $A$ : it contains $(u, u)$ , $(v, v)$ and $(w, w)$ , so it is reflexive on $A$ ; its pairs with distinct coordinates are $(u, v)$ and $(v, u)$ , and each of those has its reverse present, so it is symmetric; and every composable pair of its members has its composite present, since chains through $u$ and $v$ stay inside ${u, v}$ and $w$ relates only to itself.

L1L2L3L11L13step 1.1

3.1

The classes are as stated: $[u] = {b \in A : u \sim b} = {u, v}$ , $[v] = {u, v}$ by the pairs $(v, u)$ and $(v, v)$ , and $[w] = {w}$ . Hence $A / \sim$ has exactly the two elements ${u, v}$ and ${w}$ , which is the collection we started from.

L4L5L7L11L13step 1.1step 2.1

4.1

The collection is therefore a partition of $A$ in the sense of the classes being nonempty, covering $A$ and pairwise equal or disjoint, and it is recovered as the quotient set of the equivalence relation it induces.

L6step 2.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

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