Set theory

• Ordinals
• Cardinals

DefinitionModel of ZFC#

The ZFC universe of sets consists of the type of pre-sets, quotiented by extensional equivalence.

ZFSet.{u} : Type (u + 1)

Sources

• Mathlib documentation: ZFSet
• Source of ZFSet in Mathlib/SetTheory/ZFC/Basic.lean
• Mathlib overview: Logic and computation › Set theory

MathlibZFSet

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.