mathlib docs: set

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.

source

def pSet.type (a : pSet) :

Type u

The underlying type of a pre-set

Equations

(pSet.mk α A).type = α

source

def pSet.func (x : pSet) (a : x.type) :

pSet

The underlying pre-set family of a pre-set

Equations

(pSet.mk α A).func = A

source

theorem pSet.mk_type_func (x : pSet) :

pSet.mk x.type x.func = x

source

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

source

theorem pSet.equiv.refl (x : pSet) :

x.equiv x

source

theorem pSet.equiv.euc {x : pSet} {y : pSet} {z : pSet} (a : x.equiv y) (a_1 : z.equiv y) :

x.equiv z

source

theorem pSet.equiv.symm {x : pSet} {y : pSet} (a : x.equiv y) :

y.equiv x

source

theorem pSet.equiv.trans {x : pSet} {y : pSet} {z : pSet} (h1 : x.equiv y) (h2 : y.equiv z) :

x.equiv z

source

@[instance]

def pSet.setoid :

setoid pSet

Equations

pSet.setoid = {r := pSet.equiv, iseqv := pSet.setoid._proof_1}

source

def pSet.subset (a : pSet) (a_1 : pSet) :

Prop

Equations

(pSet.mk α A).subset (pSet.mk β B) = ∀ (a : α), ∃ (b : β), (A a).equiv (B b)

source

@[instance]

def pSet.has_subset :

has_subset pSet

Equations

pSet.has_subset = {subset := pSet.subset}

source

theorem pSet.equiv.ext (x y : pSet) :

x.equiv y ↔ x ⊆ y ∧ y ⊆ x

source

theorem pSet.subset.congr_left {x y z : pSet} (a : x.equiv y) :

x ⊆ z ↔ y ⊆ z

source

theorem pSet.subset.congr_right {x y z : pSet} (a : x.equiv y) :

z ⊆ x ↔ z ⊆ y

source

def pSet.mem (a : pSet) (a_1 : pSet) :

Prop

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

Equations

x.mem (pSet.mk β B) = ∃ (b : β), x.equiv (B b)

source

@[instance]

def pSet.has_mem :

has_mem pSet pSet

Equations

pSet.has_mem = {mem := pSet.mem}

source

theorem pSet.mem.mk {α : Type u} (A : α → pSet) (a : α) :

A a ∈ pSet.mk α A

source

theorem pSet.mem.ext {x y : pSet} (a : ∀ (w : pSet), w ∈ x ↔ w ∈ y) :

x.equiv y

source

theorem pSet.mem.congr_right {x y : pSet} (a : x.equiv y) {w : pSet} :

w ∈ x ↔ w ∈ y

source

theorem pSet.equiv_iff_mem {x y : pSet} :

x.equiv y ↔ ∀ {w : pSet}, w ∈ x ↔ w ∈ y

source

theorem pSet.mem.congr_left {x y : pSet} (a : x.equiv y) {w : pSet} :

x ∈ w ↔ y ∈ w

source

def pSet.to_set (u : pSet) :

set pSet

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

Equations

u.to_set = {x : pSet | x ∈ u}

source

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

x.equiv y ↔ x.to_set = y.to_set

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

source

@[instance]

def pSet.has_coe :

has_coe pSet (set pSet)

Equations

pSet.has_coe = {coe := pSet.to_set}

source

def pSet.empty :

pSet

The empty pre-set

Equations

pSet.empty = pSet.mk (ulift empty) (λ (e : ulift empty), pSet.empty._match_1 e)

source

@[instance]

def pSet.has_emptyc :

has_emptyc pSet

Equations

pSet.has_emptyc = {emptyc := pSet.empty}

source

@[instance]

def pSet.inhabited :

inhabited pSet

Equations

pSet.inhabited = {default := ∅}

source

theorem pSet.mem_empty (x : pSet) :

x ∉ ∅

source

def pSet.insert (a a_1 : pSet) :

pSet

Insert an element into a pre-set

Equations

u.insert (pSet.mk α A) = pSet.mk (option α) (λ (o : option α), option.rec u A o)

source

@[instance]

def pSet.has_insert :

has_insert pSet pSet

Equations

pSet.has_insert = {insert := pSet.insert}

source

@[instance]

def pSet.has_singleton :

has_singleton pSet pSet

Equations

pSet.has_singleton = {singleton := λ (s : pSet), {s}}

source

@[instance]

def pSet.is_lawful_singleton :

is_lawful_singleton pSet pSet

Equations

pSet.is_lawful_singleton = {insert_emptyc_eq := pSet.is_lawful_singleton._proof_1}

source

def pSet.of_nat (a : ℕ) :

pSet

The n-th von Neumann ordinal

Equations

pSet.of_nat (n + 1) = (pSet.of_nat n).insert (pSet.of_nat n)
pSet.of_nat 0 = ∅

source

def pSet.omega :

pSet

The von Neumann ordinal ω

Equations

pSet.omega = pSet.mk (ulift ℕ) (λ (n : ulift ℕ), pSet.of_nat n.down)

source

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

pSet

The separation operation {x ∈ a | p x}

Equations

pSet.sep p (pSet.mk α A) = pSet.mk {a // p (A a)} (λ (x : {a // p (A a)}), A x.val)

source

@[instance]

def pSet.has_sep :

has_sep pSet pSet

Equations

pSet.has_sep = {sep := pSet.sep}

source

def pSet.powerset (a : pSet) :

pSet

The powerset operator

Equations

(pSet.mk α A).powerset = pSet.mk (set α) (λ (p : set α), pSet.mk {a // p a} (λ (x : {a // p a}), A x.val))

source

theorem pSet.mem_powerset {x y : pSet} :

y ∈ x.powerset ↔ y ⊆ x

source

def pSet.Union (a : pSet) :

pSet

The set union operator

Equations

(pSet.mk α A).Union = pSet.mk (Σ (x : α), (A x).type) (λ (_x : Σ (x : α), (A x).type), pSet.Union._match_1 α A _x)
pSet.Union._match_1 α A ⟨x, y⟩ = (A x).func y

source

theorem pSet.mem_Union {x y : pSet} :

y ∈ x.Union ↔ ∃ (z : pSet) (_x : z ∈ x), y ∈ z

source

def pSet.image (f : pSet → pSet) (a : pSet) :

pSet

The image of a function

Equations

pSet.image f (pSet.mk α A) = pSet.mk α (λ (a : α), f (A a))

source

theorem pSet.mem_image {f : pSet → pSet} (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)

source

def pSet.lift (a : pSet) :

pSet

Universe lift operation

Equations

(pSet.mk α A).lift = pSet.mk (ulift α) (λ (_x : ulift α), pSet.lift._match_1 α (λ (x : α), (A x).lift) _x)
pSet.lift._match_1 α _f_1 {down := x} = _f_1 x

source

def pSet.embed :

pSet

Embedding of one universe in another

Equations

pSet.embed = pSet.mk (ulift pSet) (λ (_x : ulift pSet), pSet.embed._match_1 _x)
pSet.embed._match_1 {down := x} = x.lift

source

theorem pSet.lift_mem_embed (x : pSet) :

x.lift ∈ pSet.embed

source

def pSet.arity.equiv {n : ℕ} (a a_1 : arity 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

pSet.arity.equiv a b = ∀ (x y : pSet), x.equiv y → pSet.arity.equiv (a x) (b y)
pSet.arity.equiv a b = pSet.equiv a b

source

theorem pSet.arity.equiv_const {a : pSet} (n : ℕ) :

pSet.arity.equiv (arity.const a n) (arity.const a n)

source

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

pSet.resp n = {x // pSet.arity.equiv x x}

source

@[instance]

def pSet.resp.inhabited {n : ℕ} :

inhabited (pSet.resp n)

Equations

pSet.resp.inhabited = {default := ⟨arity.const (default pSet) n, _⟩}

source

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

pSet.resp n

Equations

f.f x = ⟨f.val x, _⟩

source

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

Prop

Equations

a.equiv b = pSet.arity.equiv a.val b.val

source

theorem pSet.resp.refl {n : ℕ} (a : pSet.resp n) :

a.equiv a

source

theorem pSet.resp.euc {n : ℕ} {a b c : pSet.resp n} (a_1 : a.equiv b) (a_2 : c.equiv b) :

a.equiv c

source

@[instance]

def pSet.resp.setoid {n : ℕ} :

setoid (pSet.resp n)

Equations

pSet.resp.setoid = {r := pSet.resp.equiv n, iseqv := _}

source

def Set :

Type (u+1)

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

Equations

Set = quotient pSet.setoid

source

def pSet.resp.eval_aux {n : ℕ} :

{f // ∀ (a b : pSet.resp n), a.equiv b → f a = f b}

Equations

pSet.resp.eval_aux = let F : pSet.resp (n + 1) → arity Set (n + 1) := λ (a : pSet.resp (n + 1)), quotient.lift (λ (x : pSet), pSet.resp.eval_aux.val (a.f x)) _ in ⟨F, _⟩
pSet.resp.eval_aux = ⟨λ (a : pSet.resp 0), ⟦a.val ⟧, pSet.resp.eval_aux._main._proof_1⟩

source

def pSet.resp.eval (n : ℕ) (a : pSet.resp n) :

arity Set n

An equivalence-respecting function yields an n-ary Set function.

Equations

pSet.resp.eval n = pSet.resp.eval_aux.val

source

theorem pSet.resp.eval_val {n : ℕ} {f : pSet.resp (n + 1)} {x : pSet} :

pSet.resp.eval (n + 1) f ⟦x⟧ = pSet.resp.eval n (f.f x)

source

@[class]

inductive pSet.definable (n : ℕ) (a : arity Set n) :

Type (u+1)

mk : Π (n : ℕ) (f : pSet.resp n), pSet.definable n (pSet.resp.eval n f)

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

source

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

pSet.definable n s

Equations

pSet.definable.eq_mk f rfl = pSet.definable.mk f

source

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

pSet.resp n

Equations

pSet.definable.resp (pSet.resp.eval n f) = f

source

theorem pSet.definable.eq {n : ℕ} (s : arity Set n) [H : pSet.definable n s] :

pSet.resp.eval n (pSet.definable.resp s) = s

source

def classical.all_definable {n : ℕ} (F : arity Set n) :

pSet.definable n F

Equations

classical.all_definable F = pSet.definable.eq_mk ⟨λ (x : pSet), (pSet.definable.resp (F ⟦x⟧)).val, _⟩ _
classical.all_definable F = let p : ∃ (a : pSet), ⟦a⟧ = F := _ in pSet.definable.eq_mk ⟨classical.some p, _⟩ _

source

def Set.mk (a : pSet) :

Set

Equations

Set.mk = quotient.mk

source

@[simp]

theorem Set.mk_eq (x : pSet) :

⟦x⟧ = Set.mk x

source

@[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)

source

def Set.mem (a a_1 : Set) :

Prop

Equations

Set.mem = quotient.lift₂ pSet.mem Set.mem._proof_1

source

@[instance]

def Set.has_mem :

has_mem Set Set

Equations

Set.has_mem = {mem := Set.mem}

source

def Set.to_set (u : Set) :

set Set

Convert a ZFC set into a set of sets

Equations

u.to_set = {x : Set | x ∈ u}

source

def Set.subset (x y : Set) :

Prop

Equations

x.subset y = ∀ ⦃z : Set⦄, z ∈ x → z ∈ y

source

@[instance]

def Set.has_subset :

has_subset Set

Equations

Set.has_subset = {subset := Set.subset}

source

theorem Set.subset_iff (x y : pSet) :

Set.mk x ⊆ Set.mk y ↔ x ⊆ y

source

theorem Set.ext {x y : Set} (a : ∀ (z : Set), z ∈ x ↔ z ∈ y) :

x = y

source

theorem Set.ext_iff {x y : Set} :

(∀ (z : Set), z ∈ x ↔ z ∈ y) ↔ x = y

source

def Set.empty :

Set

The empty set

Equations

Set.empty = Set.mk ∅

source

@[instance]

def Set.has_emptyc :

has_emptyc Set

Equations

Set.has_emptyc = {emptyc := Set.empty}

source

@[instance]

def Set.inhabited :

inhabited Set

Equations

Set.inhabited = {default := ∅}

source

@[simp]

theorem Set.mem_empty (x : Set) :

x ∉ ∅

source

theorem Set.eq_empty (x : Set) :

x = ∅ ↔ ∀ (y : Set), y ∉ x

source

def Set.insert (a a_1 : Set) :

Set

insert x y is the set {x} ∪ y

Equations

Set.insert = pSet.resp.eval 2 ⟨pSet.insert, Set.insert._proof_1⟩

source

@[instance]

def Set.has_insert :

has_insert Set Set

Equations

Set.has_insert = {insert := Set.insert}

source

@[instance]

def Set.has_singleton :

has_singleton Set Set

Equations

Set.has_singleton = {singleton := λ (x : Set), {x}}

source

@[instance]

def Set.is_lawful_singleton :

is_lawful_singleton Set Set

Equations

Set.is_lawful_singleton = {insert_emptyc_eq := Set.is_lawful_singleton._proof_1}

source

@[simp]

theorem Set.mem_insert {x y z : Set} :

x ∈ insert y z ↔ x = y ∨ x ∈ z

source

@[simp]

theorem Set.mem_singleton {x y : Set} :

x ∈ {y} ↔ x = y

source

@[simp]

theorem Set.mem_pair {x y z : Set} :

x ∈ {y, z} ↔ x = y ∨ x = z

source

def Set.omega :

Set

omega is the first infinite von Neumann ordinal

Equations

Set.omega = Set.mk pSet.omega

source

@[simp]

theorem Set.omega_zero :

∅ ∈ Set.omega

source

@[simp]

theorem Set.omega_succ {n : Set} (a : n ∈ Set.omega) :

insert n n ∈ Set.omega

source

def Set.sep (p : Set → Prop) (a : Set) :

Set

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

Equations

Set.sep p = pSet.resp.eval 1 ⟨pSet.sep (λ (y : pSet), p ⟦y⟧), _⟩

source

@[instance]

def Set.has_sep :

has_sep Set Set

Equations

Set.has_sep = {sep := Set.sep}

source

@[simp]

theorem Set.mem_sep {p : Set → Prop} {x y : Set} :

y ∈ {y ∈ x | p y} ↔ y ∈ x ∧ p y

source

def Set.powerset (a : Set) :

Set

The powerset operation, the collection of subsets of a set

Equations

Set.powerset = pSet.resp.eval 1 ⟨pSet.powerset, Set.powerset._proof_1⟩

source

@[simp]

theorem Set.mem_powerset {x y : Set} :

y ∈ x.powerset ↔ y ⊆ x

source

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)

source

def Set.Union (a : Set) :

Set

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

Equations

⋃ = pSet.resp.eval 1 ⟨pSet.Union, Set.Union._proof_1⟩

source

@[simp]

theorem Set.mem_Union {x y : Set} :

y ∈ x.Union ↔ ∃ (z : Set) (H : z ∈ x), y ∈ z

source

@[simp]

theorem Set.Union_singleton {x : Set} :

{x}.Union = x

source

theorem Set.singleton_inj {x y : Set} (H : {x} = {y}) :

x = y

source

def Set.union (x y : Set) :

Set

The binary union operation

Equations

x.union y = {x, y}.Union

source

def Set.inter (x y : Set) :

Set

The binary intersection operation

Equations

x.inter y = {z ∈ x | z ∈ y}

source

def Set.diff (x y : Set) :

Set

The set difference operation

Equations

x.diff y = {z ∈ x | z ∉ y}

source

@[instance]

def Set.has_union :

has_union Set

Equations

Set.has_union = {union := Set.union}

source

@[instance]

def Set.has_inter :

has_inter Set

Equations

Set.has_inter = {inter := Set.inter}

source

@[instance]

def Set.has_sdiff :

has_sdiff Set

Equations

Set.has_sdiff = {sdiff := Set.diff}

source

@[simp]

theorem Set.mem_union {x y z : Set} :

z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y

source

@[simp]

theorem Set.mem_inter {x y z : Set} :

z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y

source

@[simp]

theorem Set.mem_diff {x y z : Set} :

z ∈ x \ y ↔ z ∈ x ∧ z ∉ y

source

theorem Set.induction_on {p : Set → Prop} (x : Set) (h : ∀ (x : Set), (∀ (y : Set), y ∈ x → p y) → p x) :

p x

source

theorem Set.regularity (x : Set) (h : x ≠ ∅) :

∃ (y : Set) (H : y ∈ x), x ∩ y = ∅

source

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

Set

The image of a (definable) set function

Equations

Set.image f = let r : pSet.resp 1 := pSet.definable.resp f in pSet.resp.eval 1 ⟨pSet.image r.val, _⟩

source

theorem Set.image.mk (f : Set → Set) [H : pSet.definable 1 f] (x : Set) {y : Set} (h : y ∈ x) :

f y ∈ Set.image f x

source

@[simp]

theorem Set.mem_image {f : Set → Set} [H : pSet.definable 1 f] {x y : Set} :

y ∈ Set.image f x ↔ ∃ (z : Set) (H : z ∈ x), f z = y

source

def Set.pair (x y : Set) :

Set

Kuratowski ordered pair

Equations

x.pair y = {{x}, {x, y}}

source

def Set.pair_sep (p : Set → Set → Prop) (x y : Set) :

Set

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

Equations

Set.pair_sep p x y = {z ∈ (x ∪ y).powerset.powerset | ∃ (a : Set) (H : a ∈ x) (b : Set) (H : b ∈ y), z = a.pair b ∧ p a b}

source

@[simp]

theorem Set.mem_pair_sep {p : Set → Set → 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

source

theorem Set.pair_inj {x y x' y' : Set} (H : x.pair y = x'.pair y') :

x = x' ∧ y = y'

source

def Set.prod (a a_1 : Set) :

Set

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

Equations

Set.prod = Set.pair_sep (λ (a b : Set), true)

source

@[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

source

@[simp]

theorem Set.pair_mem_prod {x y a b : Set} :

a.pair b ∈ x.prod y ↔ a ∈ x ∧ b ∈ y

source

def Set.is_func (x y f : Set) :

Prop

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

Equations

x.is_func y f = (f ⊆ x.prod y ∧ ∀ (z : Set), z ∈ x → (∃! (w : Set), z.pair w ∈ f))

source

def Set.funs (x y : Set) :

Set

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

Equations

x.funs y = {f ∈ (x.prod y).powerset | x.is_func y f}

source

@[simp]

theorem Set.mem_funs {x y f : Set} :

f ∈ x.funs y ↔ x.is_func y f

source

@[instance]

def Set.map_definable_aux (f : Set → Set) [H : pSet.definable 1 f] :

pSet.definable 1 (λ (y : Set), y.pair (f y))

Equations

Set.map_definable_aux f = classical.all_definable (λ (y : Set), y.pair (f y))

source

def Set.map (f : Set → Set) [H : pSet.definable 1 f] (a : Set) :

Set

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

Equations

Set.map f = Set.image (λ (y : Set), y.pair (f y))

source

@[simp]

theorem Set.mem_map {f : Set → Set} [H : pSet.definable 1 f] {x y : Set} :

y ∈ Set.map f x ↔ ∃ (z : Set) (H : z ∈ x), z.pair (f z) = y

source

theorem Set.map_unique {f : Set → Set} [H : pSet.definable 1 f] {x z : Set} (zx : z ∈ x) :

∃! (w : Set), z.pair w ∈ Set.map f x

source

@[simp]

theorem Set.map_is_func {f : Set → Set} [H : pSet.definable 1 f] {x y : Set} :

x.is_func y (Set.map f x) ↔ ∀ (z : Set), z ∈ x → f z ∈ y

source

def Class :

Type (u_1+1)

Equations

Class = set Set

source

@[instance]

def Class.has_subset :

has_subset Class

Equations

Class.has_subset = {subset := set.subset Set}

source

@[instance]

def Class.has_sep :

has_sep Set Class

Equations

Class.has_sep = {sep := set.sep Set}

source

@[instance]

def Class.has_emptyc :

has_emptyc Class

Equations

Class.has_emptyc = {emptyc := λ (a : Set), false}

source

@[instance]

def Class.inhabited :

inhabited Class

Equations

Class.inhabited = {default := ∅}

source

@[instance]

def Class.has_insert :

has_insert Set Class

Equations

Class.has_insert = {insert := set.insert Set}

source

@[instance]

def Class.has_union :

has_union Class

Equations

Class.has_union = {union := set.union Set}

source

@[instance]

def Class.has_inter :

has_inter Class

Equations

Class.has_inter = {inter := set.inter Set}

source

@[instance]

def Class.has_neg :

has_neg Class

Equations

Class.has_neg = {neg := set.compl Set}

source

@[instance]

def Class.has_sdiff :

has_sdiff Class

Equations

Class.has_sdiff = {sdiff := set.diff Set}

source

def Class.of_Set (x : Set) :

Class

Coerce a set into a class

Equations

Class.of_Set x = {y : Set | y ∈ x}

source

@[instance]

def Class.has_coe :

has_coe Set Class

Equations

Class.has_coe = {coe := Class.of_Set}

source

def Class.univ :

Class

The universal class

Equations

Class.univ = set.univ

source

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

Prop

Assert that A is a set satisfying p

Equations

Class.to_Set p A = ∃ (x : Set), ↑x = A ∧ p x

source

def Class.mem (A B : Class) :

Prop

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

Equations

A.mem B = Class.to_Set B A

source

@[instance]

def Class.has_mem :

has_mem Class Class

Equations

Class.has_mem = {mem := Class.mem}

source

theorem Class.mem_univ {A : Class} :

A ∈ Class.univ ↔ ∃ (x : Set), ↑x = A

source

def Class.Cong_to_Class (x : set Class) :

Class

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

Equations

Class.Cong_to_Class x = {y : Set | ↑y ∈ x}

source

def Class.Class_to_Cong (x : Class) :

set Class

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

Equations

x.Class_to_Cong = {y : Class | y ∈ x}

source

def Class.powerset (x : Class) :

Class

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

Equations

x.powerset = Class.Cong_to_Class (𝒫x)

source

def Class.Union (x : Class) :

Class

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

Equations

x.Union = ⋃₀x.Class_to_Cong

source

theorem Class.of_Set.inj {x y : Set} (h : ↑x = ↑y) :

x = y

source

@[simp]

theorem Class.to_Set_of_Set (p : Set → Prop) (x : Set) :

Class.to_Set p ↑x ↔ p x

source

@[simp]

theorem Class.mem_hom_left (x : Set) (A : Class) :

↑x ∈ A ↔ A x

source

@[simp]

theorem Class.mem_hom_right (x y : Set) :

↑y x ↔ x ∈ y

source

@[simp]

theorem Class.subset_hom (x y : Set) :

↑x ⊆ ↑y ↔ x ⊆ y

source

@[simp]

theorem Class.sep_hom (p : Set → Prop) (x : Set) :

↑{y ∈ x | p y} = {y ∈ ↑x | p y}

source

@[simp]

theorem Class.empty_hom :

↑∅ = ∅

source

@[simp]

theorem Class.insert_hom (x y : Set) :

insert x ↑y = ↑(insert x y)

source

@[simp]

theorem Class.union_hom (x y : Set) :

↑x ∪ ↑y = ↑(x ∪ y)

source

@[simp]

theorem Class.inter_hom (x y : Set) :

↑x ∩ ↑y = ↑(x ∩ y)

source

@[simp]

theorem Class.diff_hom (x y : Set) :

↑x \ ↑y = ↑(x \ y)

source

@[simp]

theorem Class.powerset_hom (x : Set) :

↑x.powerset = ↑(x.powerset)

source

@[simp]

theorem Class.Union_hom (x : Set) :

↑x.Union = ↑(x.Union)

source

def Class.iota (p : Set → Prop) :

Class

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

Equations

Class.iota p = ⋃ {x : Set | ∀ (y : Set), p y ↔ y = x}

source

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

Class.iota p = ↑x

source

theorem Class.iota_ex (p : Set → Prop) :

Class.iota p ∈ Class.univ

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.

source

def Class.fval (F A : Class) :

Class

Function value

Equations