Definition·D002
Empty set
The set with no members.
In words
For every x, x is not a member of the empty set.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
The empty set
, characterized by having no members. Its existence is not assumed but proven in T01 from Separation applied to any set given by Infinity; its uniqueness is Extensionality (any two sets with no members have the same members, hence are equal).
Used by
Propose an edit4 published revisions
- 7/11/2026 · Benjamin· Fix Mathlib link: add the #doc fragment doc-gen4's find endpoint requires (old link 404'd). Content unchanged.what changed →
- 7/11/2026 · Benjamin· Restructure: refresh empty-set definition notewhat changed →
- 7/11/2026 · Benjamin· Backfill: add plain-English prose and Mathlib docs linkwhat changed →
- 7/11/2026 · Benjamin· Initial foundations seedwhat changed →