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

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

Example

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

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

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 $\varnothing$ and arbitrary sets $A$ and $B$ .

[L1]

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

[L2]

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

[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 $\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).

[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 $\varnothing$ (There is exactly one set with no elements, written $\varnothing$ ).

[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 = \varnothing$ if and only if $A = \varnothing$ or $B = \varnothing$ ( $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 \setminus C) = (A \times B) \setminus (A \times C)$ , $(A \cap B) \times (C \cap D) = (A \times C) \cap (B \times D)$ ; $A \times B = \varnothing$ if and only if $A = \varnothing$ or $B = \varnothing$ ; 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 \subsetneq y$ , and the separation notation $\{\, z \in x : \varphi(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 \mathcal{P}(\mathcal{P}(A \cup B)) : \exists a \in A\ \exists b \in B\ z = (a,b) \,\}$ ).

[L14]

if $I = \varnothing$ then $\prod_{i \in I} A_i = \{\varnothing\}$ ( $\prod_{i \in \varnothing} A_i = \{\varnothing\}$ ; if $A_j = \varnothing$ for some $j \in I$ then $\prod_{i \in I} A_i = \varnothing$ ; 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 \bigcup_{i \in I} A_i \ \mid\ f(i) \in A_i \text{ for every } i \in I \,\}$ ).

Verification

technique · direct

1.1

$\varnothing$ has no elements, so "every element is an ordered pair" holds vacuously and $\varnothing$ is a relation; $\varnothing \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 $\varnothing$ , hence so is its field.

L1L2L9L12

1.2

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

L7L8L9L11L12L13

2.1

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

L3L4L9L12step 1.1

3.1

As a function $\varnothing \to \varnothing$ 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 $\varnothing$ has none; so it is a bijection.

L5L6L9step 2.1

3.2

As a function $\varnothing \to \{\varnothing\}$ it is still injective, for the same reason, but not surjective: $\varnothing$ is an element of $\{\varnothing\}$ 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 \varnothing} A_i = \{\varnothing\}$ , and its one element is a function with domain $\varnothing$ .

L14L15step 2.1

4.1

All five descriptions hold of the single set $\varnothing$ , 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 37 results over 15 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

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)