mathlib documentation

set_theory.zfc.basic

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
Instances for arity
@[simp]
theorem arity_zero (α : Type u) :
arity α 0 = α
@[simp]
theorem arity_succ (α : Type u) (n : ) :
arity α n.succ = (α → arity α n)
def arity.const {α : Type u} (a : α) (n : ) :
arity α n

Constant n-ary function with value a.

Equations
@[simp]
theorem arity.const_zero {α : Type u} (a : α) :
@[simp]
theorem arity.const_succ {α : Type u} (a : α) (n : ) :
arity.const a n.succ = λ (_x : α), arity.const a n
theorem arity.const_succ_apply {α : Type u} (a : α) (n : ) (x : α) :
@[protected, 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.

Instances for pSet
def pSet.type  :
pSetType u

The underlying type of a pre-set

Equations
Instances for pSet.type
def pSet.func (x : pSet) :
x.typepSet

The underlying pre-set family of a pre-set

Equations
@[simp]
theorem pSet.mk_type (α : Type u_1) (A : α → pSet) :
(pSet.mk α A).type = α
@[simp]
theorem pSet.mk_func (α : Type u_1) (A : α → pSet) :
(pSet.mk α A).func = A
@[simp]
theorem pSet.eta (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_iff {x : pSet} {y : pSet} :
x.equiv y (∀ (i : x.type), ∃ (j : y.type), (x.func i).equiv (y.func j)) ∀ (j : y.type), ∃ (i : x.type), (x.func i).equiv (y.func j)
theorem pSet.equiv.exists_left {x : pSet} {y : pSet} (h : x.equiv y) (i : x.type) :
∃ (j : y.type), (x.func i).equiv (y.func j)
theorem pSet.equiv.exists_right {x : pSet} {y : pSet} (h : x.equiv y) (j : y.type) :
∃ (i : x.type), (x.func i).equiv (y.func j)
@[protected, refl]
theorem pSet.equiv.refl (x : pSet) :
x.equiv x
@[protected]
theorem pSet.equiv.rfl {x : pSet} :
x.equiv x
@[protected]
theorem pSet.equiv.euc {x : pSet} {y : pSet} {z : pSet} :
x.equiv yz.equiv yx.equiv z
@[protected, symm]
theorem pSet.equiv.symm {x : pSet} {y : pSet} :
x.equiv yy.equiv x
@[protected, trans]
theorem pSet.equiv.trans {x : pSet} {y : pSet} {z : pSet} (h1 : x.equiv y) (h2 : y.equiv z) :
x.equiv z
@[protected]
theorem pSet.equiv_of_is_empty (x : pSet) (y : pSet) [is_empty x.type] [is_empty y.type] :
x.equiv y
@[protected, instance]
Equations
@[protected]
def pSet.subset (x : pSet) (y : pSet) :
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
@[protected, instance]
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)
@[protected]
def pSet.mem (x y : pSet) :
Prop

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

Equations
@[protected, instance]
Equations
theorem pSet.mem.mk {α : Type u} (A : α → pSet) (a : α) :
A a pSet.mk α A
theorem pSet.func_mem (x : pSet) (i : x.type) :
x.func i x
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
@[protected, instance]
theorem pSet.mem_asymm {x y : pSet} :
x yy x
theorem pSet.mem_irrefl (x : pSet) :
x x
def pSet.to_set (u : pSet) :

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

Equations
@[simp]
theorem pSet.mem_to_set (a u : pSet) :
a u.to_set a u
@[protected]
def pSet.nonempty (u : pSet) :
Prop

A nonempty set is one that contains some element.

Equations
theorem pSet.nonempty_def (u : pSet) :
u.nonempty ∃ (x : pSet), x u
theorem pSet.nonempty_of_mem {x u : pSet} (h : x u) :
theorem pSet.equiv.eq {x y : pSet} :

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

@[protected, instance]
Equations
@[protected]
def pSet.empty  :

The empty pre-set

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[simp]
theorem pSet.mem_empty (x : pSet) :
@[simp]
@[simp]
theorem pSet.empty_subset (x : pSet) :
@[protected]
theorem pSet.equiv_empty (x : pSet) [is_empty x.type] :
@[protected]
def pSet.insert (x y : pSet) :

Insert an element into a pre-set

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

The n-th von Neumann ordinal

Equations
def pSet.omega  :

The von Neumann ordinal ω

Equations
@[protected]
def pSet.sep (p : pSet → Prop) (x : pSet) :

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

Equations
@[protected, instance]
Equations
def pSet.powerset (x : pSet) :

The pre-set powerset operator

Equations
@[simp]
theorem pSet.mem_powerset {x y : pSet} :
def pSet.sUnion (a : pSet) :

The pre-set union operator

Equations
@[simp]
theorem pSet.mem_sUnion {x y : pSet} :
y ⋃₀ x ∃ (z : pSet) (H : z x), y z
@[simp]
def pSet.image (f : pSetpSet) (x : pSet) :

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)
@[protected]
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
Instances for pSet.resp
@[protected, instance]
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
@[protected]
theorem pSet.resp.equiv.refl {n : } (a : pSet.resp n) :
a.equiv a
@[protected]
theorem pSet.resp.equiv.euc {n : } {a b c : pSet.resp n} :
a.equiv bc.equiv ba.equiv c
@[protected]
theorem pSet.resp.equiv.symm {n : } {a b : pSet.resp n} :
a.equiv bb.equiv a
@[protected]
theorem pSet.resp.equiv.trans {n : } {x y z : pSet.resp n} (h1 : x.equiv y) (h2 : y.equiv z) :
x.equiv z
@[protected, instance]
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
Instances for pSet.resp.eval
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 of this typeclass
Instances of other typeclasses for pSet.definable
  • pSet.definable.has_sizeof_inst
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
noncomputable def classical.all_definable {n : } (F : arity Set n) :

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.mk_out (x : Set) :
theorem Set.eq {x y : pSet} :
theorem Set.sound {x y : pSet} (h : x.equiv y) :
theorem Set.exact {x y : pSet} :
Set.mk x = Set.mk yx.equiv y
@[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)
@[protected]
def Set.mem  :
SetSet → Prop

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

Equations
@[protected, instance]
Equations
@[simp]
theorem Set.mk_mem_iff {x y : pSet} :
def Set.to_set (u : Set) :

Convert a ZFC set into a set of ZFC sets

Equations
Instances for Set.to_set
@[simp]
theorem Set.mem_to_set (a u : Set) :
a u.to_set a u
@[protected, instance]
def Set.small_to_set (x : Set) :
@[protected]
def Set.nonempty (u : Set) :
Prop

A nonempty set is one that contains some element.

Equations
theorem Set.nonempty_def (u : Set) :
u.nonempty ∃ (x : Set), x u
theorem Set.nonempty_of_mem {x u : Set} (h : x u) :
@[protected]
def Set.subset (x y : Set) :
Prop

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

Equations
@[protected, instance]
Equations
theorem Set.subset_def {x y : Set} :
x y ∀ ⦃z : Set⦄, z xz y
@[simp]
theorem Set.subset_iff {x y : pSet} :
@[simp]
theorem Set.to_set_subset_iff {x y : Set} :
@[ext]
theorem Set.ext {x y : Set} :
(∀ (z : Set), z x z y)x = y
theorem Set.ext_iff {x y : Set} :
x = y ∀ (z : Set), z x z y
@[simp]
theorem Set.to_set_inj {x y : Set} :
x.to_set = y.to_set x = y
@[protected]
def Set.empty  :

The empty ZFC set

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

insert x y is the set {x} ∪ y

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[simp]
theorem Set.mem_insert_iff {x y z : Set} :
theorem Set.mem_insert (x y : Set) :
theorem Set.mem_insert_of_mem {y z : Set} (x : Set) (h : z y) :
@[simp]
theorem Set.mem_singleton {x y : Set} :
x {y} x = y
@[simp]
theorem Set.to_set_singleton (x : Set) :
{x}.to_set = {x}
@[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]
@[protected]
def Set.sep (p : Set → Prop) :
SetSet

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

Equations
@[protected, instance]
Equations
@[simp]
theorem Set.mem_sep {p : Set → Prop} {x y : Set} :
y {y ∈ x | p y} y x p y
@[simp]
theorem Set.to_set_sep (a : Set) (p : Set → Prop) :
{x ∈ a | p x}.to_set = {x ∈ a.to_set | p x}
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.sUnion_lem {α β : Type u} (A : α → pSet) (B : β → pSet) (αβ : ∀ (a : α), ∃ (b : β), (A a).equiv (B b)) (a : (⋃₀ pSet.mk α A).type) :
∃ (b : (⋃₀ pSet.mk β B).type), ((⋃₀ pSet.mk α A).func a).equiv ((⋃₀ pSet.mk β B).func b)
def Set.sUnion  :
SetSet

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

Equations
@[simp]
theorem Set.mem_sUnion {x y : Set} :
y ⋃₀ x ∃ (z : Set) (H : z x), y z
theorem Set.mem_sUnion_of_mem {x y z : Set} (hy : y z) (hz : z x) :
@[simp]
theorem Set.sUnion_singleton {x : Set} :
⋃₀ {x} = x
@[simp]
theorem Set.singleton_inj {x y : Set} :
{x} = {y} x = y
@[simp]
@[protected]
def Set.union (x y : Set) :

The binary union operation

Equations
@[protected]
def Set.inter (x y : Set) :

The binary intersection operation

Equations
@[protected]
def Set.diff (x y : Set) :

The set difference operation

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem Set.to_set_union (x y : Set) :
@[simp]
theorem Set.to_set_inter (x y : Set) :
@[simp]
theorem Set.to_set_sdiff (x y : Set) :
(x \ y).to_set = x.to_set \ y.to_set
@[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

Induction on the relation.

@[protected, instance]
theorem Set.mem_asymm {x y : Set} :
x yy x
theorem Set.mem_irrefl (x : Set) :
x 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
@[simp]
theorem Set.to_set_image (f : SetSet) [H : pSet.definable 1 f] (x : Set) :
def Set.pair (x y : Set) :

Kuratowski ordered pair

Equations
  • x.pair y = {{x}, {x, y}}
Instances for Set.pair
@[simp]
theorem Set.to_set_pair (x y : Set) :
(x.pair y).to_set = {{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
@[simp]
theorem Set.pair_inj {x y x' y' : Set} :
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
@[protected, instance]
noncomputable def Set.map_definable_aux (f : SetSet) [H : pSet.definable 1 f] :
pSet.definable 1 (λ (y : Set), y.pair (f y))
Equations
noncomputable 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
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def Class  :
Type (u_1+1)

The collection of all classes.

We define Class as set Set, as this allows us to get many instances automatically. However, in practice, we treat it as (the definitionally equal) Set → Prop. This means, the preferred way to state that x : Set belongs to A : Class is to write A x.

Equations
Instances for Class
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def Class.of_Set (x : Set) :

Coerce a ZFC set into a class

Equations
@[protected, instance]
Equations
def Class.univ  :

The universal class

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

Assert that A is a ZFC set satisfying B

Equations
@[protected]
def Class.mem (A B : Class) :
Prop

A ∈ B if A is a ZFC set which satisfies B

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

There is no universal set.

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.sUnion (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 (A : Class) (x : Set) :
A.to_Set x A x
@[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 : Class) (x : Set) :
{y ∈ x | p y} = {y ∈ x | p y}
@[simp]
theorem Class.empty_hom  :
@[simp]
@[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.sUnion_hom (x : Set) :
def Class.iota (A : Class) :

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

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

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 ClassSet 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)
noncomputable 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) :