ExampleConstruction: Literature-sourcedVerification: 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.

$\emptyset$ is a relation on every set, is the unique equivalence relation on $\emptyset$ , is a function $\emptyset \to B$ for every $B$ , is a bijection $\emptyset \to \emptyset$ , and is not a surjection $\emptyset \to {\emptyset}$

Example

The empty set does the work of five different objects at once.

$\emptyset$ is a relation, and a relation on $A$ for every set $A$ ; its domain, range and field are all $\emptyset$ .
$\emptyset$ is the only relation on $\emptyset$ , and it is an equivalence relation on $\emptyset$ ; so $\emptyset$ carries exactly one equivalence relation.
$\emptyset$ is a function $\emptyset \to B$ for every set $B$ , and it is the only one.
$\emptyset$ is a bijection $\emptyset \to \emptyset$ .
$\emptyset$ is not a surjection $\emptyset \to {\emptyset}$ , even though it is an injective function $\emptyset \to {\emptyset}$ .

The last two together are the reason a codomain belongs to the declaration $f : A \to B$ rather than to the set $f$ : one and the same set is a bijection under one declaration and a non-surjection under another. The empty function is also the unique element of the empty product.

Facts & Assumptions

Given: the set $\emptyset$ and arbitrary sets $A$ and $B$ .

[L1]

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$ ").

[L2]

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

[L3]

A function is a relation $f$ such that $(a, b) \in f$ and $(a, c) \in f$ imply $b = c$ (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).

[L4]

We write $f : A \to B$ , and say $f$ is a function from $A$ to $B$ , when $f$ is a function with $dom f = A$ and $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).

[L5]

$f$ is injective (one-to-one) if $f (x) = f (y)$ implies $x = y$ , for all $x, y \in A$ (Injection, surjection, bijection).

[L6]

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

[L7]

A binary relation $\sim$ on $A$ is an equivalence relation when it is reflexive, symmetric and transitive (Equivalence relation, equivalence class, and the quotient set $A / \sim$ ).

[L8]

$R$ is reflexive on $A$ when $(a, a) \in R$ for every $a \in A$ (Reflexive, irreflexive, symmetric, asymmetric, antisymmetric, transitive, and connex relations on a set).

[L9]

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

[L10]

${x} : = {x, x}$ , the singleton of $x$ , is the set whose only element is $x$ (The unordered pair ${x, y}$ and the singleton ${x} = {x, x}$ ).

[L11]

$A \times B = \emptyset$ if and only if $A = \emptyset$ or $B = \emptyset$ ( $A \times (B \cup C) = (A \times B) \cup (A \times C)$ , $A \times (B \cap C) = (A \times B) \cap (A \times C)$ , $A \times (B ∖ C) = (A \times B) ∖ (A \times C)$ , $(A \cap B) \times (C \cap D) = (A \times C) \cap (B \times D)$ ; $A \times B = \emptyset$ if and only if $A = \emptyset$ or $B = \emptyset$ ; and for nonempty $A$ and $B$ , $A \times B \subseteq C \times D$ if and only if $A \subseteq C$ and $B \subseteq D$ ).

[L12]

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

[L13]

$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)}$ ).

[L14]

if $I = \emptyset$ then $\prod_{i \in I} A_{i} = {\emptyset}$ ( $\prod_{i \in \emptyset} A_{i} = {\emptyset}$ ; if $A_{j} = \emptyset$ for some $j \in I$ then $\prod_{i \in I} A_{i} = \emptyset$ ; and for $I = {j}$ the evaluation $f \mapsto f (j)$ is a bijection $\prod_{i \in I} A_{i} \to A_{j}$ ).

[L15]

an element of $\prod_{i \in I} A_{i}$ is a function with domain $I$ that takes its value at each index inside the member carried by that index (The product $\prod_{i \in I} A_{i} : = {f : I \to ⋃_{i \in I} A_{i} ∣ f (i) \in A_{i} for every i \in I}$ ).

Verification

technique · direct

1.1

$\emptyset$ has no elements, so "every element is an ordered pair" holds vacuously and $\emptyset$ is a relation; $\emptyset \subseteq A \times A$ for every $A$ , so it is a relation on every set; and no set satisfies the defining conditions for its domain or its range, so both are $\emptyset$ , hence so is its field.

L1L2L9L12

1.2

A relation on $\emptyset$ is a subset of $\emptyset \times \emptyset$ , which is $\emptyset$ , so $\emptyset$ is the only one. It is reflexive on $\emptyset$ , symmetric and transitive, since each condition quantifies over elements of $\emptyset$ ; hence it is the unique equivalence relation on $\emptyset$ .

L7L8L9L11L12L13

2.1

$\emptyset$ is single valued vacuously, has domain $\emptyset$ and range $\emptyset \subseteq B$ , so $\emptyset : \emptyset \to B$ for every $B$ ; and any function with domain $\emptyset$ has no elements, so it is $\emptyset$ .

L3L4L9L12step 1.1

3.1

As a function $\emptyset \to \emptyset$ it is injective, since the injectivity condition quantifies over elements of the domain, and surjective, since the surjectivity condition quantifies over elements of the codomain and $\emptyset$ has none; so it is a bijection.

L5L6L9step 2.1

3.2

As a function $\emptyset \to {\emptyset}$ it is still injective, for the same reason, but not surjective: $\emptyset$ is an element of ${\emptyset}$ and no element of the domain is sent to it.

L5L6L9L10step 2.1

3.3

The empty function is the unique element of the empty product: $\prod_{i \in \emptyset} A_{i} = {\emptyset}$ , and its one element is a function with domain $\emptyset$ .

L14L15step 2.1

4.1

All five descriptions hold of the single set $\emptyset$ , and the last two differ only in the declared codomain.

step 1.1step 1.2step 2.1step 3.1step 3.2step 3.3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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

B. Kaya, MATH 320 Set Theory (METU), Exercise 9 (standard reference, not scraped)
Equivalence relation (Wikipedia) (standard reference, not scraped)
Empty function (Wikipedia) (standard reference, not scraped)

∅∅ is a relation on every set, is the unique equivalence relation on ∅∅, is a function ∅→B∅→B for every BB, is a bijection ∅→∅∅→∅, and is not a surjection ∅→{∅}∅→{∅}