mathlib documentation

set_theory.zfc

def arity  :
Type uType 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  :
pSetpSet → 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.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} :
x.equiv yy.equiv zx.equiv z

@[instance]

Equations
def pSet.subset  :
pSetpSet → Prop

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} (a : 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} (a : x.equiv y) {w : pSet} :
x w y w

def pSet.to_set  :

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.

@[instance]

Equations
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
@[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  :
set pSetpSetpSet

The separation operation {x ∈ a | p x}

Equations
@[instance]

Equations
def pSet.powerset  :

The powerset operator

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

def pSet.Union  :

The set union operator

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

def pSet.image  :
(pSetpSet)pSetpSet

The image of a function

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
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  :
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 : } :
pSet.resp (n + 1)pSetpSet.resp n

Equations
def pSet.resp.equiv {n : } :
pSet.resp npSet.resp n → Prop

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}

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

An equivalence-respecting function yields an n-ary 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 Set.mk  :
pSetSet

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

Equations
@[instance]

Equations
def Set.to_set  :
Setset Set

Convert a ZFC set into a set of sets

Equations
def Set.subset  :
SetSet → Prop

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 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
@[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  :
(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 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 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} :
{x} = {y}x = y

def Set.union  :
SetSetSet

The binary union operation

Equations
def Set.inter  :
SetSetSet

The binary intersection operation

Equations
def Set.diff  :
SetSetSet

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) :
(∀ (x : Set), (∀ (y : Set), y xp y)p x)p x

theorem Set.regularity (x : Set) :
x (∃ (y : Set) (H : y x), x y = )

def Set.image (f : SetSet) [H : pSet.definable 1 f] :
SetSet

The image of a (definable) set function

Equations
theorem Set.image.mk (f : SetSet) [H : pSet.definable 1 f] (x : Set) {y : Set} :
y xf 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  :
SetSetSet

Kuratowski ordered pair

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

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} :
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  :
SetSetSet → Prop

is_func x y f is the assertion f : x → y where f is a ZFC function (a set of ordered pairs)

Equations
def Set.funs  :
SetSetSet

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} :
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)

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
def Class.of_Set  :

Coerce a set into a class

Equations
@[instance]

Equations
def Class.univ  :

The universal class

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

Assert that A is a set satisfying p

Equations
def Class.mem  :
ClassClass → Prop

A ∈ B if A is a 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  :

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

Equations
def Class.Union  :

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

Equations
theorem Class.of_Set.inj {x y : Set} :
x = yx = 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  :
(Set → Prop)Class

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

Equations
theorem Class.iota_val (p : Set → Prop) (x : Set) :
(∀ (y : Set), p y y = x)Class.iota p = 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  :
ClassClassClass

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} :
y x(Set.map f x)y = (f y)

def Set.choice  :
SetSet

A choice function on the set of nonempty sets x

Equations
theorem Set.choice_mem_aux (x : Set) (h : x) (y : Set) :
y xclassical.epsilon (λ (z : Set), z y) y

theorem Set.choice_is_func (x : Set) :
xx.is_func x.Union x.choice

theorem Set.choice_mem (x : Set) (h : x) (y : Set) :
y x(x.choice)y y