mathlib documentation

set_theory.zfc

A model of ZFC #

In this file, we model Zermelo-Fraenkel set theory (+ Choice) using Lean's underlying type theory. We do this in four main steps:

The model #

Other definitions #

Notes #

To avoid confusion between the Lean set and the ZFC Set, docstrings in this file refer to them respectively as "set" and "ZFC set".

TODO #

Prove Set.map_definable_aux computably.

def arity (α : Type u) :
Type u

The type of n-ary functions α → α → ... → α.

Equations
def arity.const {α : Type u} (a : α) (n : ) :
arity α n

Constant n-ary function with value a.

Equations
@[instance]
def arity.arity.inhabited {α : Type u_1} {n : } [inhabited α] :
Equations
inductive pSet  :
Type (u+1)
  • mk : Π (α : Type ?), (α → pSet)pSet

The type of pre-sets in universe u. A pre-set is a family of pre-sets indexed by a type in Type u. The ZFC universe is defined as a quotient of this to ensure extensionality.

def pSet.type  :
pSetType u

The underlying type of a pre-set

Equations
def pSet.func (x : pSet) :
x.typepSet

The underlying pre-set family of a pre-set

Equations
theorem pSet.mk_type_func (x : pSet) :
def pSet.equiv (x : pSet) (y : pSet) :
Prop

Two pre-sets are extensionally equivalent if every element of the first family is extensionally equivalent to some element of the second family and vice-versa.

Equations
  • x.equiv y = pSet.rec (λ (α : Type u_1) (z : α → pSet) (m : α → pSet → Prop) (_x : pSet), pSet.equiv._match_1 α m _x) x y
  • pSet.equiv._match_1 α m (pSet.mk β B) = ((∀ (a : α), ∃ (b : β), m a (B b)) ∀ (b : β), ∃ (a : α), m a (B b))
theorem pSet.equiv.refl (x : pSet) :
x.equiv x
theorem pSet.equiv.rfl {x : pSet} :
x.equiv x
theorem pSet.equiv.euc {x : pSet} {y : pSet} {z : pSet} :
x.equiv yz.equiv yx.equiv z
theorem pSet.equiv.symm {x : pSet} {y : pSet} :
x.equiv yy.equiv x
theorem pSet.equiv.trans {x : pSet} {y : pSet} {z : pSet} (h1 : x.equiv y) (h2 : y.equiv z) :
x.equiv z
@[instance]
Equations
def pSet.subset  :
pSetpSet → Prop

A pre-set is a subset of another pre-set if every element of the first family is extensionally equivalent to some element of the second family.

Equations
theorem pSet.equiv.ext (x y : pSet) :
x.equiv y x y y x
theorem pSet.subset.congr_left {x y z : pSet} :
x.equiv y(x z y z)
theorem pSet.subset.congr_right {x y z : pSet} :
x.equiv y(z x z y)
def pSet.mem  :
pSetpSet → Prop

x ∈ y as pre-sets if x is extensionally equivalent to a member of the family y.

Equations
@[instance]
Equations
theorem pSet.mem.mk {α : Type u} (A : α → pSet) (a : α) :
A a pSet.mk α A
theorem pSet.mem.ext {x y : pSet} :
(∀ (w : pSet), w x w y)x.equiv y
theorem pSet.mem.congr_right {x y : pSet} :
x.equiv y∀ {w : pSet}, w x w y
theorem pSet.equiv_iff_mem {x y : pSet} :
x.equiv y ∀ {w : pSet}, w x w y
theorem pSet.mem.congr_left {x y : pSet} :
x.equiv y∀ {w : pSet}, x w y w
def pSet.to_set (u : pSet) :

Convert a pre-set to a set of pre-sets.

Equations
theorem pSet.equiv.eq {x y : pSet} :

Two pre-sets are equivalent iff they have the same members.

def pSet.empty  :

The empty pre-set

Equations
@[instance]
Equations
theorem pSet.mem_empty (x : pSet) :
def pSet.insert  :
pSetpSetpSet

Insert an element into a pre-set

Equations
@[instance]
Equations
def pSet.of_nat  :
pSet

The n-th von Neumann ordinal

Equations
def pSet.omega  :

The von Neumann ordinal ω

Equations
def pSet.sep (p : set pSet) :

The pre-set separation operation {x ∈ a | p x}

Equations
@[instance]
Equations
def pSet.powerset  :

The pre-set powerset operator

Equations
theorem pSet.mem_powerset {x y : pSet} :
def pSet.Union  :

The pre-set union operator

Equations
theorem pSet.mem_Union {x y : pSet} :
y x.Union ∃ (z : pSet) (_x : z x), y z
def pSet.image (f : pSetpSet) :

The image of a function from pre-sets to pre-sets.

Equations
theorem pSet.mem_image {f : pSetpSet} (H : ∀ {x y : pSet}, x.equiv y(f x).equiv (f y)) {x y : pSet} :
y pSet.image f x ∃ (z : pSet) (H : z x), y.equiv (f z)
def pSet.lift  :

Universe lift operation

Equations
@[nolint]
def pSet.embed  :

Embedding of one universe in another

Equations
def pSet.arity.equiv {n : } :
arity pSet narity pSet n → Prop

Function equivalence is defined so that f ~ g iff ∀ x y, x ~ y → f x ~ g y. This extends to equivalence of n-ary functions.

Equations
def pSet.resp (n : ) :
Type (u+1)

resp n is the collection of n-ary functions on pSet that respect equivalence, i.e. when the inputs are equivalent the output is as well.

Equations
def pSet.resp.f {n : } (f : pSet.resp (n + 1)) (x : pSet) :

The n-ary image of a (n + 1)-ary function respecting equivalence as a function respecting equivalence.

Equations
def pSet.resp.equiv {n : } (a b : pSet.resp n) :
Prop

Function equivalence for functions respecting equivalence. See pSet.arity.equiv.

Equations
theorem pSet.resp.refl {n : } (a : pSet.resp n) :
a.equiv a
theorem pSet.resp.euc {n : } {a b c : pSet.resp n} :
a.equiv bc.equiv ba.equiv c
@[instance]
Equations
def Set  :
Type (u+1)

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

Equations
def pSet.resp.eval_aux {n : } :
{f // ∀ (a b : pSet.resp n), a.equiv bf a = f b}

Helper function for pSet.eval.

Equations
def pSet.resp.eval (n : ) :

An equivalence-respecting function yields an n-ary ZFC set function.

Equations
theorem pSet.resp.eval_val {n : } {f : pSet.resp (n + 1)} {x : pSet} :
@[class]
inductive pSet.definable (n : ) :
arity Set nType (u+1)

A set function is "definable" if it is the image of some n-ary pre-set function. This isn't exactly definability, but is useful as a sufficient condition for functions that have a computable image.

Instances
def pSet.definable.eq_mk {n : } (f : pSet.resp n) {s : arity Set n} (H : pSet.resp.eval n f = s) :

The evaluation of a function respecting equivalence is definable, by that same function.

Equations
def pSet.definable.resp {n : } (s : arity Set n) [pSet.definable n s] :

Turns a definable function into a function that respects equivalence.

Equations

All functions are classically definable.

Equations
def Set.mk  :
pSetSet

Turns a pre-set into a ZFC set.

Equations
@[simp]
theorem Set.mk_eq (x : pSet) :
@[simp]
theorem Set.eval_mk {n : } {f : pSet.resp (n + 1)} {x : pSet} :
pSet.resp.eval (n + 1) f (Set.mk x) = pSet.resp.eval n (f.f x)
def Set.mem  :
SetSet → Prop

The membership relation for ZFC sets is inherited from the membership relation for pre-sets.

Equations
@[instance]
Equations
def Set.to_set (u : Set) :

Convert a ZFC set into a set of ZFC sets

Equations
def Set.subset (x y : Set) :
Prop

x ⊆ y as ZFC sets means that all members of x are members of y.

Equations
theorem Set.subset_def {x y : Set} :
x y ∀ ⦃z : Set⦄, z xz y
theorem Set.subset_iff (x y : pSet) :
theorem Set.ext {x y : Set} :
(∀ (z : Set), z x z y)x = y
theorem Set.ext_iff {x y : Set} :
(∀ (z : Set), z x z y) x = y
def Set.empty  :

The empty ZFC set

Equations
@[instance]
Equations
@[instance]
Equations
@[simp]
theorem Set.mem_empty (x : Set) :
theorem Set.eq_empty (x : Set) :
x = ∀ (y : Set), y x
def Set.insert  :
SetSetSet

insert x y is the set {x} ∪ y

Equations
@[instance]
Equations
@[simp]
theorem Set.mem_insert {x y z : Set} :
x insert y z x = y x z
@[simp]
theorem Set.mem_singleton {x y : Set} :
x {y} x = y
@[simp]
theorem Set.mem_pair {x y z : Set} :
x {y, z} x = y x = z
def Set.omega  :

omega is the first infinite von Neumann ordinal

Equations
@[simp]
@[simp]
theorem Set.omega_succ {n : Set} :
def Set.sep (p : Set → Prop) :
SetSet

{x ∈ a | p x} is the set of elements in a satisfying p

Equations
@[instance]
Equations
@[simp]
theorem Set.mem_sep {p : Set → Prop} {x y : Set} :
y {y ∈ x | p y} y x p y
def Set.powerset  :
SetSet

The powerset operation, the collection of subsets of a ZFC set

Equations
@[simp]
theorem Set.mem_powerset {x y : Set} :
theorem Set.Union_lem {α β : Type u} (A : α → pSet) (B : β → pSet) (αβ : ∀ (a : α), ∃ (b : β), (A a).equiv (B b)) (a : (pSet.mk α A).Union.type) :
∃ (b : (pSet.mk β B).Union.type), ((pSet.mk α A).Union.func a).equiv ((pSet.mk β B).Union.func b)
def Set.Union  :
SetSet

The union operator, the collection of elements of elements of a ZFC set

Equations
@[simp]
theorem Set.mem_Union {x y : Set} :
y x.Union ∃ (z : Set) (H : z x), y z
@[simp]
theorem Set.Union_singleton {x : Set} :
{x}.Union = x
theorem Set.singleton_inj {x y : Set} (H : {x} = {y}) :
x = y
def Set.union (x y : Set) :

The binary union operation

Equations
def Set.inter (x y : Set) :

The binary intersection operation

Equations
def Set.diff (x y : Set) :

The set difference operation

Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[simp]
theorem Set.mem_union {x y z : Set} :
z x y z x z y
@[simp]
theorem Set.mem_inter {x y z : Set} :
z x y z x z y
@[simp]
theorem Set.mem_diff {x y z : Set} :
z x \ y z x z y
theorem Set.induction_on {p : Set → Prop} (x : Set) (h : ∀ (x : Set), (∀ (y : Set), y xp y)p x) :
p x
theorem Set.regularity (x : Set) (h : x ) :
∃ (y : Set) (H : y x), x y =
def Set.image (f : SetSet) [H : pSet.definable 1 f] :
SetSet

The image of a (definable) ZFC set function

Equations
theorem Set.image.mk (f : SetSet) [H : pSet.definable 1 f] (x : Set) {y : Set} (h : y x) :
f y Set.image f x
@[simp]
theorem Set.mem_image {f : SetSet} [H : pSet.definable 1 f] {x y : Set} :
y Set.image f x ∃ (z : Set) (H : z x), f z = y
def Set.pair (x y : Set) :

Kuratowski ordered pair

Equations
  • x.pair y = {{x}, {x, y}}
def Set.pair_sep (p : SetSet → Prop) (x y : Set) :

A subset of pairs {(a, b) ∈ x × y | p a b}

Equations
@[simp]
theorem Set.mem_pair_sep {p : SetSet → Prop} {x y z : Set} :
z Set.pair_sep p x y ∃ (a : Set) (H : a x) (b : Set) (H : b y), z = a.pair b p a b
theorem Set.pair_inj {x y x' y' : Set} (H : x.pair y = x'.pair y') :
x = x' y = y'
def Set.prod  :
SetSetSet

The cartesian product, {(a, b) | a ∈ x, b ∈ y}

Equations
@[simp]
theorem Set.mem_prod {x y z : Set} :
z x.prod y ∃ (a : Set) (H : a x) (b : Set) (H : b y), z = a.pair b
@[simp]
theorem Set.pair_mem_prod {x y a b : Set} :
a.pair b x.prod y a x b y
def Set.is_func (x y f : Set) :
Prop

is_func x y f is the assertion that f is a subset of x × y which relates to each element of x a unique element of y, so that we can consider fas a ZFC function x → y.

Equations
def Set.funs (x y : Set) :

funs x y is y ^ x, the set of all set functions x → y

Equations
@[simp]
theorem Set.mem_funs {x y f : Set} :
f x.funs y x.is_func y f
@[instance]
def Set.map_definable_aux (f : SetSet) [H : pSet.definable 1 f] :
pSet.definable 1 (λ (y : Set), y.pair (f y))
Equations
def Set.map (f : SetSet) [H : pSet.definable 1 f] :
SetSet

Graph of a function: map f x is the ZFC function which maps a ∈ x to f a

Equations
@[simp]
theorem Set.mem_map {f : SetSet} [H : pSet.definable 1 f] {x y : Set} :
y Set.map f x ∃ (z : Set) (H : z x), z.pair (f z) = y
theorem Set.map_unique {f : SetSet} [H : pSet.definable 1 f] {x z : Set} (zx : z x) :
∃! (w : Set), z.pair w Set.map f x
@[simp]
theorem Set.map_is_func {f : SetSet} [H : pSet.definable 1 f] {x y : Set} :
x.is_func y (Set.map f x) ∀ (z : Set), z xf z y
def Class  :
Type (u_1+1)

The collection of all classes. A class is defined as a set of ZFC sets.

Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
def Class.of_Set (x : Set) :

Coerce a ZFC set into a class

Equations
@[instance]
Equations
def Class.univ  :

The universal class

Equations
def Class.to_Set (p : Set → Prop) (A : Class) :
Prop

Assert that A is a ZFC set satisfying p

Equations
def Class.mem (A B : Class) :
Prop

A ∈ B if A is a ZFC set which is a member of B

Equations
@[instance]
Equations
theorem Class.mem_univ {A : Class} :
A Class.univ ∃ (x : Set), x = A

Convert a conglomerate (a collection of classes) into a class

Equations

Convert a class into a conglomerate (a collection of classes)

Equations
def Class.powerset (x : Class) :

The power class of a class is the class of all subclasses that are ZFC sets

Equations
def Class.Union (x : Class) :

The union of a class is the class of all members of ZFC sets in the class

Equations
theorem Class.of_Set.inj {x y : Set} (h : x = y) :
x = y
@[simp]
theorem Class.to_Set_of_Set (p : Set → Prop) (x : Set) :
@[simp]
theorem Class.mem_hom_left (x : Set) (A : Class) :
x A A x
@[simp]
theorem Class.mem_hom_right (x y : Set) :
y x x y
@[simp]
theorem Class.subset_hom (x y : Set) :
x y x y
@[simp]
theorem Class.sep_hom (p : Set → Prop) (x : Set) :
{y ∈ x | p y} = {y ∈ x | p y}
@[simp]
theorem Class.empty_hom  :
@[simp]
theorem Class.insert_hom (x y : Set) :
@[simp]
theorem Class.union_hom (x y : Set) :
x y = (x y)
@[simp]
theorem Class.inter_hom (x y : Set) :
x y = (x y)
@[simp]
theorem Class.diff_hom (x y : Set) :
x \ y = (x \ y)
@[simp]
@[simp]
theorem Class.Union_hom (x : Set) :
def Class.iota (p : Set → Prop) :

The definite description operator, which is {x} if {a | p a} = {x} and otherwise.

Equations
theorem Class.iota_val (p : Set → Prop) (x : Set) (H : ∀ (y : Set), p y y = x) :
theorem Class.iota_ex (p : Set → Prop) :

Unlike the other set constructors, the iota definite descriptor is a set for any set input, but not constructively so, so there is no associated (Set → Prop) → Set function.

def Class.fval (F A : Class) :

Function value

Equations
theorem Class.fval_ex (F A : Class) :
@[simp]
theorem Set.map_fval {f : SetSet} [H : pSet.definable 1 f] {x y : Set} (h : y x) :
(Set.map f x)y = (f y)
def Set.choice (x : Set) :

A choice function on the class of nonempty ZFC sets.

Equations
theorem Set.choice_mem_aux (x : Set) (h : x) (y : Set) (yx : y x) :
classical.epsilon (λ (z : Set), z y) y
theorem Set.choice_is_func (x : Set) (h : x) :
theorem Set.choice_mem (x : Set) (h : x) (y : Set) (yx : y x) :