Documentation

inductive PSet :

Type (u + 1)

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.

mk: (α : Type u) → (α → PSet) → PSet

Instances For

def PSet.Type :

PSet → Type u

The underlying type of a pre-set

Equations

PSet.Type x = match x with | PSet.mk α A => α

Instances For

def PSet.Func (x : PSet) :

PSet.Type x → PSet

The underlying pre-set family of a pre-set

Equations

PSet.Func x = match (motive := (x : PSet) → PSet.Type x → PSet) x with | PSet.mk α A => A

Instances For

@[simp]

theorem PSet.mk_type (α : Type u_1) (A : α → PSet) :

PSet.Type (PSet.mk α A) = α

@[simp]

theorem PSet.mk_func (α : Type u_1) (A : α → PSet) :

PSet.Func (PSet.mk α A) = A

@[simp]

theorem PSet.eta (x : PSet) :

PSet.mk (PSet.Type x) (PSet.Func x) = x

def PSet.Equiv :

PSet → 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

PSet.Equiv (PSet.mk α A) (PSet.mk α_1 B) = ((∀ (a : α), ∃ (b : α_1), PSet.Equiv (A a) (B b)) ∧ ∀ (b : α_1), ∃ (a : α), PSet.Equiv (A a) (B b))

Instances For

theorem PSet.equiv_iff {x : PSet} {y : PSet} :

PSet.Equiv x y ↔ (∀ (i : PSet.Type x), ∃ (j : PSet.Type y), PSet.Equiv (PSet.Func x i) (PSet.Func y j)) ∧ ∀ (j : PSet.Type y), ∃ (i : PSet.Type x), PSet.Equiv (PSet.Func x i) (PSet.Func y j)

theorem PSet.Equiv.exists_left {x : PSet} {y : PSet} (h : PSet.Equiv x y) (i : PSet.Type x) :

∃ (j : PSet.Type y), PSet.Equiv (PSet.Func x i) (PSet.Func y j)

theorem PSet.Equiv.exists_right {x : PSet} {y : PSet} (h : PSet.Equiv x y) (j : PSet.Type y) :

∃ (i : PSet.Type x), PSet.Equiv (PSet.Func x i) (PSet.Func y j)

theorem PSet.Equiv.refl (x : PSet) :

PSet.Equiv x x

theorem PSet.Equiv.rfl {x : PSet} :

PSet.Equiv x x

theorem PSet.Equiv.euc {x : PSet} {y : PSet} {z : PSet} :

PSet.Equiv x y → PSet.Equiv z y → PSet.Equiv x z

theorem PSet.Equiv.symm {x : PSet} {y : PSet} :

PSet.Equiv x y → PSet.Equiv y x

theorem PSet.Equiv.comm {x : PSet} {y : PSet} :

PSet.Equiv x y ↔ PSet.Equiv y x

theorem PSet.Equiv.trans {x : PSet} {y : PSet} {z : PSet} (h1 : PSet.Equiv x y) (h2 : PSet.Equiv y z) :

PSet.Equiv x z

theorem PSet.equiv_of_isEmpty (x : PSet) (y : PSet) [IsEmpty (PSet.Type x)] [IsEmpty (PSet.Type y)] :

PSet.Equiv x y

instance PSet.setoid :

Setoid PSet

Equations

PSet.setoid = { r := PSet.Equiv, iseqv := PSet.setoid.proof_1 }

def PSet.Subset (x : PSet) (y : PSet) :

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

PSet.Subset x y = ∀ (a : PSet.Type x), ∃ (b : PSet.Type y), PSet.Equiv (PSet.Func x a) (PSet.Func y b)

Instances For

instance PSet.instHasSubsetPSet :

HasSubset PSet

Equations

PSet.instHasSubsetPSet = { Subset := PSet.Subset }

instance PSet.instIsReflPSetSubsetInstHasSubsetPSet :

IsRefl PSet fun (x x_1 : PSet) => x ⊆ x_1

Equations

PSet.instIsReflPSetSubsetInstHasSubsetPSet = ⋯

instance PSet.instIsTransPSetSubsetInstHasSubsetPSet :

IsTrans PSet fun (x x_1 : PSet) => x ⊆ x_1

Equations

PSet.instIsTransPSetSubsetInstHasSubsetPSet = ⋯

theorem PSet.Equiv.ext (x : PSet) (y : PSet) :

PSet.Equiv x y ↔ x ⊆ y ∧ y ⊆ x

theorem PSet.Subset.congr_left {x : PSet} {y : PSet} {z : PSet} :

PSet.Equiv x y → (x ⊆ z ↔ y ⊆ z)

theorem PSet.Subset.congr_right {x : PSet} {y : PSet} {z : PSet} :

PSet.Equiv x y → (z ⊆ x ↔ z ⊆ y)

def PSet.Mem (x : PSet) (y : PSet) :

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

Equations

PSet.Mem x y = ∃ (b : PSet.Type y), PSet.Equiv x (PSet.Func y b)

Instances For

instance PSet.instMembershipPSetPSet :

Membership PSet PSet

Equations

PSet.instMembershipPSetPSet = { mem := PSet.Mem }

theorem PSet.Mem.mk {α : Type u} (A : α → PSet) (a : α) :

A a ∈ PSet.mk α A

theorem PSet.func_mem (x : PSet) (i : PSet.Type x) :

PSet.Func x i ∈ x

theorem PSet.Mem.ext {x : PSet} {y : PSet} :

(∀ (w : PSet), w ∈ x ↔ w ∈ y) → PSet.Equiv x y

theorem PSet.Mem.congr_right {x : PSet} {y : PSet} :

PSet.Equiv x y → ∀ {w : PSet}, w ∈ x ↔ w ∈ y

theorem PSet.equiv_iff_mem {x : PSet} {y : PSet} :

PSet.Equiv x y ↔ ∀ {w : PSet}, w ∈ x ↔ w ∈ y

theorem PSet.Mem.congr_left {x : PSet} {y : PSet} :

PSet.Equiv x y → ∀ {w : PSet}, x ∈ w ↔ y ∈ w

theorem PSet.mem_wf :

WellFounded fun (x x_1 : PSet) => x ∈ x_1

instance PSet.instWellFoundedRelationPSet :

WellFoundedRelation PSet

Equations

PSet.instWellFoundedRelationPSet = { rel := fun (x x_1 : PSet) => x ∈ x_1, wf := PSet.mem_wf }

instance PSet.instIsAsymmPSetMemInstMembershipPSetPSet :

IsAsymm PSet fun (x x_1 : PSet) => x ∈ x_1

Equations

PSet.instIsAsymmPSetMemInstMembershipPSetPSet = ⋯

instance PSet.instIsIrreflPSetMemInstMembershipPSetPSet :

IsIrrefl PSet fun (x x_1 : PSet) => x ∈ x_1

Equations

PSet.instIsIrreflPSetMemInstMembershipPSetPSet = ⋯

theorem PSet.mem_asymm {x : PSet} {y : PSet} :

x ∈ y → y ∉ x

theorem PSet.mem_irrefl (x : PSet) :

x ∉ x

def PSet.toSet (u : PSet) :

Set PSet

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

Equations

PSet.toSet u = {x : PSet | x ∈ u}

Instances For

@[simp]

theorem PSet.mem_toSet (a : PSet) (u : PSet) :

a ∈ PSet.toSet u ↔ a ∈ u

def PSet.Nonempty (u : PSet) :

A nonempty set is one that contains some element.

Equations

PSet.Nonempty u = Set.Nonempty (PSet.toSet u)

Instances For

theorem PSet.nonempty_def (u : PSet) :

PSet.Nonempty u ↔ ∃ (x : PSet), x ∈ u

theorem PSet.nonempty_of_mem {x : PSet} {u : PSet} (h : x ∈ u) :

PSet.Nonempty u

@[simp]

theorem PSet.nonempty_toSet_iff {u : PSet} :

Set.Nonempty (PSet.toSet u) ↔ PSet.Nonempty u

theorem PSet.nonempty_type_iff_nonempty {x : PSet} :

Nonempty (PSet.Type x) ↔ PSet.Nonempty x

theorem PSet.nonempty_of_nonempty_type (x : PSet) [h : Nonempty (PSet.Type x)] :

PSet.Nonempty x

theorem PSet.Equiv.eq {x : PSet} {y : PSet} :

PSet.Equiv x y ↔ PSet.toSet x = PSet.toSet y

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

instance PSet.instCoePSetSetPSet :

Coe PSet (Set PSet)

Equations

PSet.instCoePSetSetPSet = { coe := PSet.toSet }

def PSet.empty :

The empty pre-set

Equations

PSet.empty = PSet.mk PEmpty.{u_1 + 1} PEmpty.elim

Instances For

instance PSet.instEmptyCollectionPSet :

EmptyCollection PSet

Equations

PSet.instEmptyCollectionPSet = { emptyCollection := PSet.empty }

instance PSet.instInhabitedPSet :

Inhabited PSet

Equations

PSet.instInhabitedPSet = { default := ∅ }

instance PSet.instIsEmptyTypeEmptyCollectionPSetInstEmptyCollectionPSet :

IsEmpty (PSet.Type ∅)

Equations

PSet.instIsEmptyTypeEmptyCollectionPSetInstEmptyCollectionPSet = ⋯

@[simp]

theorem PSet.not_mem_empty (x : PSet) :

x ∉ ∅

@[simp]

theorem PSet.toSet_empty :

PSet.toSet ∅ = ∅

@[simp]

theorem PSet.empty_subset (x : PSet) :

∅ ⊆ x

@[simp]

theorem PSet.not_nonempty_empty :

¬PSet.Nonempty ∅

theorem PSet.equiv_empty (x : PSet) [IsEmpty (PSet.Type x)] :

PSet.Equiv x ∅

def PSet.insert (x : PSet) (y : PSet) :

Insert an element into a pre-set

Equations

PSet.insert x y = PSet.mk (Option (PSet.Type y)) fun (o : Option (PSet.Type y)) => Option.casesOn o x (PSet.Func y)

Instances For

instance PSet.instInsertPSetPSet :

Insert PSet PSet

Equations

PSet.instInsertPSetPSet = { insert := PSet.insert }

instance PSet.instSingletonPSetPSet :

Singleton PSet PSet

Equations

PSet.instSingletonPSetPSet = { singleton := fun (s : PSet) => insert s ∅ }

IsLawfulSingleton PSet PSet

instance PSet.instIsLawfulSingletonPSetInstEmptyCollectionPSetInstInsertPSetPSetInstSingletonPSetPSet :

Equations

PSet.instIsLawfulSingletonPSetInstEmptyCollectionPSetInstInsertPSetPSetInstSingletonPSetPSet = ⋯

instance PSet.instInhabitedTypeInsertPSetInstInsertPSetPSet (x : PSet) (y : PSet) :

Inhabited (PSet.Type (insert x y))

Equations

PSet.instInhabitedTypeInsertPSetInstInsertPSetPSet x y = inferInstanceAs (Inhabited (Option (PSet.Type y)))

def PSet.ofNat :

ℕ → PSet

The n-th von Neumann ordinal

Equations

PSet.ofNat 0 = ∅
PSet.ofNat (Nat.succ n) = insert (PSet.ofNat n) (PSet.ofNat n)

Instances For

def PSet.omega :

The von Neumann ordinal ω

Equations

PSet.omega = PSet.mk (ULift.{u_1, 0} ℕ) fun (n : ULift.{u_1, 0} ℕ) => PSet.ofNat n.down

Instances For

def PSet.sep (p : PSet → Prop) (x : PSet) :

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

Equations

PSet.sep p x = PSet.mk { a : PSet.Type x // p (PSet.Func x a) } fun (y : { a : PSet.Type x // p (PSet.Func x a) }) => PSet.Func x ↑y

Instances For

instance PSet.instSepPSetPSet :

Sep PSet PSet

Equations

PSet.instSepPSetPSet = { sep := PSet.sep }

def PSet.powerset (x : PSet) :

The pre-set powerset operator

Equations

PSet.powerset x = PSet.mk (Set (PSet.Type x)) fun (p : Set (PSet.Type x)) => PSet.mk { a : PSet.Type x // p a } fun (y : { a : PSet.Type x // p a }) => PSet.Func x ↑y

Instances For

@[simp]

theorem PSet.mem_powerset {x : PSet} {y : PSet} :

y ∈ PSet.powerset x ↔ y ⊆ x

def PSet.sUnion (a : PSet) :

The pre-set union operator

Equations

One or more equations did not get rendered due to their size.

Instances For

def PSet.«term⋃₀_» :

The pre-set union operator

Equations

PSet.«term⋃₀_» = Lean.ParserDescr.node `PSet.term⋃₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))

Instances For

@[simp]

theorem PSet.mem_sUnion {x : PSet} {y : PSet} :

y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z

@[simp]

theorem PSet.toSet_sUnion (x : PSet) :

PSet.toSet (⋃₀ x) = ⋃₀ (PSet.toSet '' PSet.toSet x)

def PSet.image (f : PSet → PSet) (x : PSet) :

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

Equations

PSet.image f x = PSet.mk (PSet.Type x) (f ∘ PSet.Func x)

Instances For

theorem PSet.mem_image {f : PSet → PSet} (H : ∀ (x y : PSet), PSet.Equiv x y → PSet.Equiv (f x) (f y)) {x : PSet} {y : PSet} :

y ∈ PSet.image f x ↔ ∃ z ∈ x, PSet.Equiv y (f z)

def PSet.Lift :

PSet → PSet

Universe lift operation

Equations

PSet.Lift (PSet.mk α A) = PSet.mk (ULift.{?u.130, ?u.131} α) fun (x : ULift.{?u.130, ?u.131} α) => match x with | { down := x } => PSet.Lift (A x)

Instances For

def PSet.embed :

Embedding of one universe in another

Equations

PSet.embed = PSet.mk (ULift.{v, u + 1} PSet) fun (x : ULift.{v, u + 1} PSet) => match x with | { down := x } => PSet.Lift x

Instances For

theorem PSet.lift_mem_embed (x : PSet) :

PSet.Lift x ∈ PSet.embed

def PSet.Arity.Equiv {n : ℕ} :

Function.OfArity PSet PSet n → Function.OfArity PSet 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 = PSet.Equiv a b
PSet.Arity.Equiv a b = ∀ (x y : PSet), PSet.Equiv x y → PSet.Arity.Equiv (a x) (b y)

Instances For

theorem PSet.Arity.equiv_const {a : PSet} (n : ℕ) :

PSet.Arity.Equiv (Function.OfArity.const PSet a n) (Function.OfArity.const PSet a n)

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 : Function.OfArity PSet PSet n // PSet.Arity.Equiv x x }

Instances For

instance PSet.Resp.inhabited {n : ℕ} :

Inhabited (PSet.Resp n)

Equations

PSet.Resp.inhabited = { default := { val := Function.OfArity.const PSet default n, property := ⋯ } }

def PSet.Resp.f {n : ℕ} (f : PSet.Resp (n + 1)) (x : PSet) :

PSet.Resp n

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

Equations

PSet.Resp.f f x = { val := ↑f x, property := ⋯ }

Instances For

def PSet.Resp.Equiv {n : ℕ} (a : PSet.Resp n) (b : PSet.Resp n) :

Function equivalence for functions respecting equivalence. See PSet.Arity.Equiv.

Equations

PSet.Resp.Equiv a b = PSet.Arity.Equiv ↑a ↑b

Instances For

theorem PSet.Resp.Equiv.refl {n : ℕ} (a : PSet.Resp n) :

PSet.Resp.Equiv a a

theorem PSet.Resp.Equiv.euc {n : ℕ} {a : PSet.Resp n} {b : PSet.Resp n} {c : PSet.Resp n} :

PSet.Resp.Equiv a b → PSet.Resp.Equiv c b → PSet.Resp.Equiv a c

theorem PSet.Resp.Equiv.symm {n : ℕ} {a : PSet.Resp n} {b : PSet.Resp n} :

PSet.Resp.Equiv a b → PSet.Resp.Equiv b a

theorem PSet.Resp.Equiv.trans {n : ℕ} {x : PSet.Resp n} {y : PSet.Resp n} {z : PSet.Resp n} (h1 : PSet.Resp.Equiv x y) (h2 : PSet.Resp.Equiv y z) :

PSet.Resp.Equiv x z

instance PSet.Resp.setoid {n : ℕ} :

Setoid (PSet.Resp n)

Equations

PSet.Resp.setoid = { r := PSet.Resp.Equiv, iseqv := ⋯ }

def ZFSet :

Type (u + 1)

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

Equations

ZFSet = Quotient PSet.setoid

Instances For

def PSet.Resp.evalAux {n : ℕ} :

{ f : PSet.Resp n → Function.OfArity ZFSet ZFSet n // ∀ (a b : PSet.Resp n), PSet.Resp.Equiv a b → f a = f b }

Helper function for PSet.eval.

Equations

PSet.Resp.evalAux = { val := fun (a : PSet.Resp 0) => ⟦↑a⟧, property := PSet.Resp.evalAux.proof_4 }
PSet.Resp.evalAux = let F := fun (a : PSet.Resp (n + 1)) => Quotient.lift (fun (x : PSet) => ↑PSet.Resp.evalAux (PSet.Resp.f a x)) ⋯; { val := F, property := ⋯ }

Instances For

def PSet.Resp.eval (n : ℕ) :

PSet.Resp n → Function.OfArity ZFSet ZFSet n

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

Equations

PSet.Resp.eval n = ↑PSet.Resp.evalAux

Instances For

theorem PSet.Resp.eval_val {n : ℕ} {f : PSet.Resp (n + 1)} {x : PSet} :

PSet.Resp.eval (n + 1) f ⟦x⟧ = PSet.Resp.eval n (PSet.Resp.f f x)

class inductive PSet.Definable (n : ℕ) :

Function.OfArity ZFSet ZFSet n → Type (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.

mk: {n : ℕ} → (f : PSet.Resp n) → PSet.Definable n (PSet.Resp.eval n f)

Instances

def PSet.Definable.EqMk {n : ℕ} (f : PSet.Resp n) {s : Function.OfArity ZFSet ZFSet n} :

PSet.Resp.eval n f = s → PSet.Definable n s

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

Equations

PSet.Definable.EqMk f x = match x✝, x with | .(PSet.Resp.eval n f), ⋯ => PSet.Definable.mk f

Instances For

def PSet.Definable.Resp {n : ℕ} (s : Function.OfArity ZFSet ZFSet n) [PSet.Definable n s] :

PSet.Resp n

Turns a definable function into a function that respects equivalence.

Equations

PSet.Definable.Resp x✝ = match x✝, x with | .(PSet.Resp.eval n f), PSet.Definable.mk f => f

Instances For

theorem PSet.Definable.eq {n : ℕ} (s : Function.OfArity ZFSet ZFSet n) [H : PSet.Definable n s] :

PSet.Resp.eval n (PSet.Definable.Resp s) = s

noncomputable def Classical.allDefinable {n : ℕ} (F : Function.OfArity ZFSet ZFSet n) :

PSet.Definable n F

All functions are classically definable.

Equations

Classical.allDefinable F = let p := ⋯; PSet.Definable.EqMk { val := Classical.choose p, property := ⋯ } ⋯
Classical.allDefinable F = let_fun I := fun (x : ZFSet) => Classical.allDefinable (F x); PSet.Definable.EqMk { val := fun (x : PSet) => ↑(PSet.Definable.Resp (F ⟦x⟧)), property := ⋯ } ⋯

Instances For

def ZFSet.mk :

PSet → ZFSet

Turns a pre-set into a ZFC set.

Equations

ZFSet.mk = Quotient.mk''

Instances For

@[simp]

theorem ZFSet.mk_eq (x : PSet) :

⟦x⟧ = ZFSet.mk x

@[simp]

theorem ZFSet.mk_out (x : ZFSet) :

ZFSet.mk (Quotient.out x) = x

theorem ZFSet.eq {x : PSet} {y : PSet} :

ZFSet.mk x = ZFSet.mk y ↔ PSet.Equiv x y

theorem ZFSet.sound {x : PSet} {y : PSet} (h : PSet.Equiv x y) :

ZFSet.mk x = ZFSet.mk y

theorem ZFSet.exact {x : PSet} {y : PSet} :

ZFSet.mk x = ZFSet.mk y → PSet.Equiv x y

@[simp]

theorem ZFSet.eval_mk {n : ℕ} {f : PSet.Resp (n + 1)} {x : PSet} :

PSet.Resp.eval (n + 1) f (ZFSet.mk x) = PSet.Resp.eval n (PSet.Resp.f f x)

def ZFSet.Mem :

ZFSet → ZFSet → Prop

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

Equations

ZFSet.Mem = Quotient.lift₂ PSet.Mem ZFSet.Mem.proof_1

Instances For

instance ZFSet.instMembershipZFSetZFSet :

Membership ZFSet ZFSet

Equations

ZFSet.instMembershipZFSetZFSet = { mem := ZFSet.Mem }

@[simp]

theorem ZFSet.mk_mem_iff {x : PSet} {y : PSet} :

ZFSet.mk x ∈ ZFSet.mk y ↔ x ∈ y

def ZFSet.toSet (u : ZFSet) :

Set ZFSet

Convert a ZFC set into a Set of ZFC sets

Equations

ZFSet.toSet u = {x : ZFSet | x ∈ u}

Instances For

@[simp]

theorem ZFSet.mem_toSet (a : ZFSet) (u : ZFSet) :

a ∈ ZFSet.toSet u ↔ a ∈ u

instance ZFSet.small_toSet (x : ZFSet) :

Small.{u, u + 1} ↑(ZFSet.toSet x)

Equations

⋯ = ⋯

def ZFSet.Nonempty (u : ZFSet) :

A nonempty set is one that contains some element.

Equations

ZFSet.Nonempty u = Set.Nonempty (ZFSet.toSet u)

Instances For

theorem ZFSet.nonempty_def (u : ZFSet) :

ZFSet.Nonempty u ↔ ∃ (x : ZFSet), x ∈ u

theorem ZFSet.nonempty_of_mem {x : ZFSet} {u : ZFSet} (h : x ∈ u) :

ZFSet.Nonempty u

@[simp]

theorem ZFSet.nonempty_toSet_iff {u : ZFSet} :

Set.Nonempty (ZFSet.toSet u) ↔ ZFSet.Nonempty u

def ZFSet.Subset (x : ZFSet) (y : ZFSet) :

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

Equations

ZFSet.Subset x y = ∀ ⦃z : ZFSet⦄, z ∈ x → z ∈ y

Instances For

instance ZFSet.hasSubset :

HasSubset ZFSet

Equations

ZFSet.hasSubset = { Subset := ZFSet.Subset }

theorem ZFSet.subset_def {x : ZFSet} {y : ZFSet} :

x ⊆ y ↔ ∀ ⦃z : ZFSet⦄, z ∈ x → z ∈ y

instance ZFSet.instIsReflZFSetSubsetHasSubset :

IsRefl ZFSet fun (x x_1 : ZFSet) => x ⊆ x_1

Equations

ZFSet.instIsReflZFSetSubsetHasSubset = ⋯

instance ZFSet.instIsTransZFSetSubsetHasSubset :

IsTrans ZFSet fun (x x_1 : ZFSet) => x ⊆ x_1

Equations

ZFSet.instIsTransZFSetSubsetHasSubset = ⋯

@[simp]

theorem ZFSet.subset_iff {x : PSet} {y : PSet} :

ZFSet.mk x ⊆ ZFSet.mk y ↔ x ⊆ y

@[simp]

theorem ZFSet.toSet_subset_iff {x : ZFSet} {y : ZFSet} :

ZFSet.toSet x ⊆ ZFSet.toSet y ↔ x ⊆ y

theorem ZFSet.ext {x : ZFSet} {y : ZFSet} :

(∀ (z : ZFSet), z ∈ x ↔ z ∈ y) → x = y

theorem ZFSet.ext_iff {x : ZFSet} {y : ZFSet} :

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

Function.Injective ZFSet.toSet

theorem ZFSet.toSet_injective :

@[simp]

theorem ZFSet.toSet_inj {x : ZFSet} {y : ZFSet} :

ZFSet.toSet x = ZFSet.toSet y ↔ x = y

instance ZFSet.instIsAntisymmZFSetSubsetHasSubset :

IsAntisymm ZFSet fun (x x_1 : ZFSet) => x ⊆ x_1

Equations

ZFSet.instIsAntisymmZFSetSubsetHasSubset = ⋯

def ZFSet.empty :

The empty ZFC set

Equations

ZFSet.empty = ZFSet.mk ∅

Instances For

instance ZFSet.instEmptyCollectionZFSet :

EmptyCollection ZFSet

Equations

ZFSet.instEmptyCollectionZFSet = { emptyCollection := ZFSet.empty }

instance ZFSet.instInhabitedZFSet :

Inhabited ZFSet

Equations

ZFSet.instInhabitedZFSet = { default := ∅ }

@[simp]

theorem ZFSet.not_mem_empty (x : ZFSet) :

x ∉ ∅

@[simp]

theorem ZFSet.toSet_empty :

ZFSet.toSet ∅ = ∅

@[simp]

theorem ZFSet.empty_subset (x : ZFSet) :

∅ ⊆ x

@[simp]

theorem ZFSet.not_nonempty_empty :

¬ZFSet.Nonempty ∅

@[simp]

theorem ZFSet.nonempty_mk_iff {x : PSet} :

ZFSet.Nonempty (ZFSet.mk x) ↔ PSet.Nonempty x

theorem ZFSet.eq_empty (x : ZFSet) :

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

theorem ZFSet.eq_empty_or_nonempty (u : ZFSet) :

u = ∅ ∨ ZFSet.Nonempty u

def ZFSet.Insert :

ZFSet → ZFSet → ZFSet

Insert x y is the set {x} ∪ y

Equations

ZFSet.Insert = PSet.Resp.eval 2 { val := PSet.insert, property := ZFSet.Insert.proof_1 }

Instances For

instance ZFSet.instInsertZFSetZFSet :

Insert ZFSet ZFSet

Equations

ZFSet.instInsertZFSetZFSet = { insert := ZFSet.Insert }

instance ZFSet.instSingletonZFSetZFSet :

Singleton ZFSet ZFSet

Equations

ZFSet.instSingletonZFSetZFSet = { singleton := fun (x : ZFSet) => insert x ∅ }

instance ZFSet.instIsLawfulSingletonZFSetInstEmptyCollectionZFSetInstInsertZFSetZFSetInstSingletonZFSetZFSet :

IsLawfulSingleton ZFSet ZFSet

Equations

ZFSet.instIsLawfulSingletonZFSetInstEmptyCollectionZFSetInstInsertZFSetZFSetInstSingletonZFSetZFSet = ⋯

@[simp]

theorem ZFSet.mem_insert_iff {x : ZFSet} {y : ZFSet} {z : ZFSet} :

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

theorem ZFSet.mem_insert (x : ZFSet) (y : ZFSet) :

x ∈ insert x y

theorem ZFSet.mem_insert_of_mem {y : ZFSet} {z : ZFSet} (x : ZFSet) (h : z ∈ y) :

z ∈ insert x y

@[simp]

theorem ZFSet.toSet_insert (x : ZFSet) (y : ZFSet) :

ZFSet.toSet (insert x y) = insert x (ZFSet.toSet y)

@[simp]

theorem ZFSet.mem_singleton {x : ZFSet} {y : ZFSet} :

x ∈ {y} ↔ x = y

@[simp]

theorem ZFSet.toSet_singleton (x : ZFSet) :

ZFSet.toSet {x} = {x}

theorem ZFSet.insert_nonempty (u : ZFSet) (v : ZFSet) :

ZFSet.Nonempty (insert u v)

theorem ZFSet.singleton_nonempty (u : ZFSet) :

ZFSet.Nonempty {u}

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

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

def ZFSet.omega :

omega is the first infinite von Neumann ordinal

Equations

ZFSet.omega = ZFSet.mk PSet.omega

Instances For

@[simp]

theorem ZFSet.omega_zero :

∅ ∈ ZFSet.omega

@[simp]

theorem ZFSet.omega_succ {n : ZFSet} :

n ∈ ZFSet.omega → insert n n ∈ ZFSet.omega

def ZFSet.sep (p : ZFSet → Prop) :

ZFSet → ZFSet

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

Equations

ZFSet.sep p = PSet.Resp.eval 1 { val := PSet.sep fun (y : PSet) => p (ZFSet.mk y), property := ⋯ }

Instances For

instance ZFSet.instSepZFSetZFSet :

Sep ZFSet ZFSet

Equations

ZFSet.instSepZFSetZFSet = { sep := ZFSet.sep }

@[simp]

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

y ∈ ZFSet.sep p x ↔ y ∈ x ∧ p y

@[simp]

theorem ZFSet.toSet_sep (a : ZFSet) (p : ZFSet → Prop) :

ZFSet.toSet (ZFSet.sep p a) = {x : ZFSet | x ∈ ZFSet.toSet a ∧ p x}

def ZFSet.powerset :

ZFSet → ZFSet

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

Equations

ZFSet.powerset = PSet.Resp.eval 1 { val := PSet.powerset, property := ZFSet.powerset.proof_1 }

Instances For

@[simp]

theorem ZFSet.mem_powerset {x : ZFSet} {y : ZFSet} :

y ∈ ZFSet.powerset x ↔ y ⊆ x

theorem ZFSet.sUnion_lem {α : Type u} {β : Type u} (A : α → PSet) (B : β → PSet) (αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv (A a) (B b)) (a : PSet.Type (⋃₀ PSet.mk α A)) :

∃ (b : PSet.Type (⋃₀ PSet.mk β B)), PSet.Equiv (PSet.Func (⋃₀ PSet.mk α A) a) (PSet.Func (⋃₀ PSet.mk β B) b)

def ZFSet.sUnion :

ZFSet → ZFSet

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

Equations

ZFSet.sUnion = PSet.Resp.eval 1 { val := PSet.sUnion, property := ZFSet.sUnion.proof_1 }

Instances For

def ZFSet.«term⋃₀_» :

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

Equations

ZFSet.«term⋃₀_» = Lean.ParserDescr.node `ZFSet.term⋃₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))

Instances For

noncomputable def ZFSet.sInter (x : ZFSet) :

The intersection operator, the collection of elements in all of the elements of a ZFC set. We special-case ⋂₀ ∅ = ∅.

Equations

⋂₀ x = if h : ZFSet.Nonempty x then ZFSet.sep (fun (y : ZFSet) => ∀ z ∈ x, y ∈ z) (Set.Nonempty.some h) else ∅

Instances For

def ZFSet.«term⋂₀_» :

The intersection operator, the collection of elements in all of the elements of a ZFC set. We special-case ⋂₀ ∅ = ∅.

Equations

ZFSet.«term⋂₀_» = Lean.ParserDescr.node `ZFSet.term⋂₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂₀ ") (Lean.ParserDescr.cat `term 110))

Instances For

@[simp]

theorem ZFSet.mem_sUnion {x : ZFSet} {y : ZFSet} :

y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z

theorem ZFSet.mem_sInter {x : ZFSet} {y : ZFSet} (h : ZFSet.Nonempty x) :

y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

@[simp]

theorem ZFSet.sUnion_empty :

⋃₀ ∅ = ∅

@[simp]

theorem ZFSet.sInter_empty :

⋂₀ ∅ = ∅

theorem ZFSet.mem_of_mem_sInter {x : ZFSet} {y : ZFSet} {z : ZFSet} (hy : y ∈ ⋂₀ x) (hz : z ∈ x) :

y ∈ z

theorem ZFSet.mem_sUnion_of_mem {x : ZFSet} {y : ZFSet} {z : ZFSet} (hy : y ∈ z) (hz : z ∈ x) :

y ∈ ⋃₀ x

theorem ZFSet.not_mem_sInter_of_not_mem {x : ZFSet} {y : ZFSet} {z : ZFSet} (hy : y ∉ z) (hz : z ∈ x) :

y ∉ ⋂₀ x

@[simp]

theorem ZFSet.sUnion_singleton {x : ZFSet} :

⋃₀ {x} = x

@[simp]

theorem ZFSet.sInter_singleton {x : ZFSet} :

⋂₀ {x} = x

@[simp]

theorem ZFSet.toSet_sUnion (x : ZFSet) :

ZFSet.toSet (⋃₀ x) = ⋃₀ (ZFSet.toSet '' ZFSet.toSet x)

theorem ZFSet.toSet_sInter {x : ZFSet} (h : ZFSet.Nonempty x) :

ZFSet.toSet (⋂₀ x) = ⋂₀ (ZFSet.toSet '' ZFSet.toSet x)

theorem ZFSet.singleton_injective :

Function.Injective singleton

@[simp]

theorem ZFSet.singleton_inj {x : ZFSet} {y : ZFSet} :

{x} = {y} ↔ x = y

def ZFSet.union (x : ZFSet) (y : ZFSet) :

The binary union operation

Equations

ZFSet.union x y = ⋃₀ {x, y}

Instances For

def ZFSet.inter (x : ZFSet) (y : ZFSet) :

The binary intersection operation

Equations

ZFSet.inter x y = ZFSet.sep (fun (z : ZFSet) => z ∈ y) x

Instances For

def ZFSet.diff (x : ZFSet) (y : ZFSet) :

The set difference operation

Equations

ZFSet.diff x y = ZFSet.sep (fun (z : ZFSet) => z ∉ y) x

Instances For

instance ZFSet.instUnionZFSet :

Union ZFSet

Equations

ZFSet.instUnionZFSet = { union := ZFSet.union }

instance ZFSet.instInterZFSet :

Inter ZFSet

Equations

ZFSet.instInterZFSet = { inter := ZFSet.inter }

instance ZFSet.instSDiffZFSet :

SDiff ZFSet

Equations

ZFSet.instSDiffZFSet = { sdiff := ZFSet.diff }

@[simp]

theorem ZFSet.toSet_union (x : ZFSet) (y : ZFSet) :

ZFSet.toSet (x ∪ y) = ZFSet.toSet x ∪ ZFSet.toSet y

@[simp]

theorem ZFSet.toSet_inter (x : ZFSet) (y : ZFSet) :

ZFSet.toSet (x ∩ y) = ZFSet.toSet x ∩ ZFSet.toSet y

@[simp]

theorem ZFSet.toSet_sdiff (x : ZFSet) (y : ZFSet) :

ZFSet.toSet (x \ y) = ZFSet.toSet x \ ZFSet.toSet y

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem ZFSet.sUnion_pair {x : ZFSet} {y : ZFSet} :

⋃₀ {x, y} = x ∪ y

theorem ZFSet.mem_wf :

WellFounded fun (x x_1 : ZFSet) => x ∈ x_1

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

p x

Induction on the ∈ relation.

WellFoundedRelation ZFSet

instance ZFSet.instWellFoundedRelationZFSet :

Equations

ZFSet.instWellFoundedRelationZFSet = { rel := fun (x x_1 : ZFSet) => x ∈ x_1, wf := ZFSet.mem_wf }

instance ZFSet.instIsAsymmZFSetMemInstMembershipZFSetZFSet :

IsAsymm ZFSet fun (x x_1 : ZFSet) => x ∈ x_1

Equations

ZFSet.instIsAsymmZFSetMemInstMembershipZFSetZFSet = ⋯

instance ZFSet.instIsIrreflZFSetMemInstMembershipZFSetZFSet :

IsIrrefl ZFSet fun (x x_1 : ZFSet) => x ∈ x_1

Equations

ZFSet.instIsIrreflZFSetMemInstMembershipZFSetZFSet = ⋯

theorem ZFSet.mem_asymm {x : ZFSet} {y : ZFSet} :

x ∈ y → y ∉ x

theorem ZFSet.mem_irrefl (x : ZFSet) :

x ∉ x

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

∃ y ∈ x, x ∩ y = ∅

def ZFSet.image (f : ZFSet → ZFSet) [PSet.Definable 1 f] :

ZFSet → ZFSet

The image of a (definable) ZFC set function

Equations

ZFSet.image f = match (motive := PSet.Resp 1 → ZFSet → ZFSet) PSet.Definable.Resp f with | { val := r, property := hr } => PSet.Resp.eval 1 { val := PSet.image r, property := ⋯ }

Instances For

theorem ZFSet.image.mk (f : ZFSet → ZFSet) [H : PSet.Definable 1 f] (x : ZFSet) {y : ZFSet} :

y ∈ x → f y ∈ ZFSet.image f x

@[simp]

theorem ZFSet.mem_image {f : ZFSet → ZFSet} [H : PSet.Definable 1 f] {x : ZFSet} {y : ZFSet} :

y ∈ ZFSet.image f x ↔ ∃ z ∈ x, f z = y

@[simp]

theorem ZFSet.toSet_image (f : ZFSet → ZFSet) [H : PSet.Definable 1 f] (x : ZFSet) :

ZFSet.toSet (ZFSet.image f x) = f '' ZFSet.toSet x

noncomputable def ZFSet.range {α : Type u} (f : α → ZFSet) :

The range of an indexed family of sets. The universes allow for a more general index type without manual use of ULift.

Equations

ZFSet.range f = ⟦PSet.mk (ULift.{v, u} α) (Quotient.out ∘ f ∘ ULift.down)⟧

Instances For

@[simp]

theorem ZFSet.mem_range {α : Type u} {f : α → ZFSet} {x : ZFSet} :

x ∈ ZFSet.range f ↔ x ∈ Set.range f

@[simp]

theorem ZFSet.toSet_range {α : Type u} (f : α → ZFSet) :

ZFSet.toSet (ZFSet.range f) = Set.range f

def ZFSet.pair (x : ZFSet) (y : ZFSet) :

Kuratowski ordered pair

Equations

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

Instances For

@[simp]

theorem ZFSet.toSet_pair (x : ZFSet) (y : ZFSet) :

ZFSet.toSet (ZFSet.pair x y) = {{x}, {x, y}}

def ZFSet.pairSep (p : ZFSet → ZFSet → Prop) (x : ZFSet) (y : ZFSet) :

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

Equations

ZFSet.pairSep p x y = ZFSet.sep (fun (z : ZFSet) => ∃ a ∈ x, ∃ b ∈ y, z = ZFSet.pair a b ∧ p a b) (ZFSet.powerset (ZFSet.powerset (x ∪ y)))

Instances For

@[simp]

theorem ZFSet.mem_pairSep {p : ZFSet → ZFSet → Prop} {x : ZFSet} {y : ZFSet} {z : ZFSet} :

z ∈ ZFSet.pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = ZFSet.pair a b ∧ p a b

Function.Injective2 ZFSet.pair

theorem ZFSet.pair_injective :

@[simp]

theorem ZFSet.pair_inj {x : ZFSet} {y : ZFSet} {x' : ZFSet} {y' : ZFSet} :

ZFSet.pair x y = ZFSet.pair x' y' ↔ x = x' ∧ y = y'

def ZFSet.prod :

ZFSet → ZFSet → ZFSet

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

Equations

ZFSet.prod = ZFSet.pairSep fun (x x : ZFSet) => True

Instances For

@[simp]

theorem ZFSet.mem_prod {x : ZFSet} {y : ZFSet} {z : ZFSet} :

z ∈ ZFSet.prod x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = ZFSet.pair a b

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

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

def ZFSet.IsFunc (x : ZFSet) (y : ZFSet) (f : ZFSet) :

isFunc 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 f as a ZFC function x → y.

Equations

ZFSet.IsFunc x y f = (f ⊆ ZFSet.prod x y ∧ ∀ z ∈ x, ∃! w : ZFSet, ZFSet.pair z w ∈ f)

Instances For

def ZFSet.funs (x : ZFSet) (y : ZFSet) :

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

Equations

ZFSet.funs x y = ZFSet.sep (ZFSet.IsFunc x y) (ZFSet.powerset (ZFSet.prod x y))

Instances For

@[simp]

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

f ∈ ZFSet.funs x y ↔ ZFSet.IsFunc x y f

noncomputable instance ZFSet.mapDefinableAux (f : ZFSet → ZFSet) [PSet.Definable 1 f] :

PSet.Definable 1 fun (y : ZFSet) => ZFSet.pair y (f y)

Equations

ZFSet.mapDefinableAux f = Classical.allDefinable fun (y : ZFSet) => ZFSet.pair y (f y)

noncomputable def ZFSet.map (f : ZFSet → ZFSet) [PSet.Definable 1 f] :

ZFSet → ZFSet

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

Equations

ZFSet.map f = ZFSet.image fun (y : ZFSet) => ZFSet.pair y (f y)

Instances For

@[simp]

theorem ZFSet.mem_map {f : ZFSet → ZFSet} [PSet.Definable 1 f] {x : ZFSet} {y : ZFSet} :

y ∈ ZFSet.map f x ↔ ∃ z ∈ x, ZFSet.pair z (f z) = y

theorem ZFSet.map_unique {f : ZFSet → ZFSet} [H : PSet.Definable 1 f] {x : ZFSet} {z : ZFSet} (zx : z ∈ x) :

∃! w : ZFSet, ZFSet.pair z w ∈ ZFSet.map f x

@[simp]

theorem ZFSet.map_isFunc {f : ZFSet → ZFSet} [PSet.Definable 1 f] {x : ZFSet} {y : ZFSet} :

ZFSet.IsFunc x y (ZFSet.map f x) ↔ ∀ z ∈ x, f z ∈ y

def ZFSet.Hereditarily (p : ZFSet → Prop) (x : ZFSet) :

Given a predicate p on ZFC sets. Hereditarily p x means that x has property p and the members of x are all Hereditarily p.

Equations

ZFSet.Hereditarily p x = (p x ∧ ∀ y ∈ x, ZFSet.Hereditarily p y)

Instances For

theorem ZFSet.hereditarily_iff {p : ZFSet → Prop} {x : ZFSet} :

ZFSet.Hereditarily p x ↔ p x ∧ ∀ y ∈ x, ZFSet.Hereditarily p y

theorem ZFSet.Hereditarily.def {p : ZFSet → Prop} {x : ZFSet} :

ZFSet.Hereditarily p x → p x ∧ ∀ y ∈ x, ZFSet.Hereditarily p y

Alias of the forward direction of ZFSet.hereditarily_iff.

theorem ZFSet.Hereditarily.self {p : ZFSet → Prop} {x : ZFSet} (h : ZFSet.Hereditarily p x) :

p x

theorem ZFSet.Hereditarily.mem {p : ZFSet → Prop} {x : ZFSet} {y : ZFSet} (h : ZFSet.Hereditarily p x) (hy : y ∈ x) :

ZFSet.Hereditarily p y

theorem ZFSet.Hereditarily.empty {p : ZFSet → Prop} {x : ZFSet} :

ZFSet.Hereditarily p x → p ∅

def Class :

Type (u_1 + 1)

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

Equations

Class = Set ZFSet

Instances For

instance instInsertZFSetClass :

Insert ZFSet Class

Equations

instInsertZFSetClass = { insert := Set.insert }

def Class.sep (p : ZFSet → Prop) (A : Class) :

{x ∈ A | p x} is the class of elements in A satisfying p

Equations

Class.sep p A = {y : ZFSet | A y ∧ p y}

Instances For

theorem Class.ext {x : Class} {y : Class} :

(∀ (z : ZFSet), x z ↔ y z) → x = y

theorem Class.ext_iff {x : Class} {y : Class} :

x = y ↔ ∀ (z : ZFSet), x z ↔ y z

def Class.ofSet (x : ZFSet) :

Coerce a ZFC set into a class

Equations

↑x = {y : ZFSet | y ∈ x}

Instances For

instance Class.instCoeZFSetClass :

Coe ZFSet Class

Equations

Class.instCoeZFSetClass = { coe := Class.ofSet }

def Class.univ :

The universal class

Equations

Class.univ = Set.univ

Instances For

def Class.ToSet (B : Class) (A : Class) :

Assert that A is a ZFC set satisfying B

Equations

Class.ToSet B A = ∃ (x : ZFSet), ↑x = A ∧ B x

Instances For

def Class.Mem (A : Class) (B : Class) :

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

Equations

Class.Mem A B = Class.ToSet B A

Instances For

instance Class.instMembershipClassClass :

Membership Class Class

Equations

Class.instMembershipClassClass = { mem := Class.Mem }

theorem Class.mem_def (A : Class) (B : Class) :

A ∈ B ↔ ∃ (x : ZFSet), ↑x = A ∧ B x

@[simp]

theorem Class.not_mem_empty (x : Class) :

x ∉ ∅

@[simp]

theorem Class.not_empty_hom (x : ZFSet) :

¬∅ x

@[simp]

theorem Class.mem_univ {A : Class} :

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

@[simp]

theorem Class.mem_univ_hom (x : ZFSet) :

Class.univ x

theorem Class.eq_univ_iff_forall {A : Class} :

A = Class.univ ↔ ∀ (x : ZFSet), A x

theorem Class.eq_univ_of_forall {A : Class} :

(∀ (x : ZFSet), A x) → A = Class.univ

theorem Class.mem_wf :

WellFounded fun (x x_1 : Class) => x ∈ x_1

WellFoundedRelation Class

instance Class.instWellFoundedRelationClass :

Equations

Class.instWellFoundedRelationClass = { rel := fun (x x_1 : Class) => x ∈ x_1, wf := Class.mem_wf }

instance Class.instIsAsymmClassMemInstMembershipClassClass :

IsAsymm Class fun (x x_1 : Class) => x ∈ x_1

Equations

Class.instIsAsymmClassMemInstMembershipClassClass = ⋯

instance Class.instIsIrreflClassMemInstMembershipClassClass :

IsIrrefl Class fun (x x_1 : Class) => x ∈ x_1

Equations

Class.instIsIrreflClassMemInstMembershipClassClass = ⋯

theorem Class.mem_asymm {x : Class} {y : Class} :

x ∈ y → y ∉ x

theorem Class.mem_irrefl (x : Class) :

x ∉ x

theorem Class.univ_not_mem_univ :

Class.univ ∉ Class.univ

There is no universal set. This is stated as univ ∉ univ, meaning that univ (the class of all sets) is proper (does not belong to the class of all sets).

def Class.congToClass (x : Set Class) :

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

Equations

Class.congToClass x = {y : ZFSet | ↑y ∈ x}

Instances For

@[simp]

theorem Class.congToClass_empty :

Class.congToClass ∅ = ∅

def Class.classToCong (x : Class) :

Set Class

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

Equations

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

Instances For

@[simp]

theorem Class.classToCong_empty :

Class.classToCong ∅ = ∅

def Class.powerset (x : Class) :

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

Equations

Class.powerset x = Class.congToClass (𝒫 x)

Instances For

def Class.sUnion (x : Class) :

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

Equations

⋃₀ x = ⋃₀ Class.classToCong x

Instances For

def Class.«term⋃₀_» :

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

Equations

Class.«term⋃₀_» = Lean.ParserDescr.node `Class.term⋃₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))

Instances For

def Class.sInter (x : Class) :

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

Equations

⋂₀ x = ⋂₀ Class.classToCong x

Instances For

def Class.«term⋂₀_» :

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

Equations

Class.«term⋂₀_» = Lean.ParserDescr.node `Class.term⋂₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂₀ ") (Lean.ParserDescr.cat `term 110))

Instances For

theorem Class.ofSet.inj {x : ZFSet} {y : ZFSet} (h : ↑x = ↑y) :

x = y

@[simp]

theorem Class.toSet_of_ZFSet (A : Class) (x : ZFSet) :

Class.ToSet A ↑x ↔ A x

@[simp]

theorem Class.coe_mem {x : ZFSet} {A : Class} :

↑x ∈ A ↔ A x

@[simp]

theorem Class.coe_apply {x : ZFSet} {y : ZFSet} :

↑y x ↔ x ∈ y

@[simp]

theorem Class.coe_subset (x : ZFSet) (y : ZFSet) :

↑x ⊆ ↑y ↔ x ⊆ y

@[simp]

theorem Class.coe_sep (p : Class) (x : ZFSet) :

↑(ZFSet.sep p x) = {y : ZFSet | y ∈ x ∧ p y}

@[simp]

theorem Class.coe_empty :

↑∅ = ∅

@[simp]

theorem Class.coe_insert (x : ZFSet) (y : ZFSet) :

↑(insert x y) = insert x ↑y

@[simp]

theorem Class.coe_union (x : ZFSet) (y : ZFSet) :

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

@[simp]

theorem Class.coe_inter (x : ZFSet) (y : ZFSet) :

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

@[simp]

theorem Class.coe_diff (x : ZFSet) (y : ZFSet) :

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

@[simp]

theorem Class.coe_powerset (x : ZFSet) :

↑(ZFSet.powerset x) = Class.powerset ↑x

@[simp]

theorem Class.powerset_apply {A : Class} {x : ZFSet} :

Class.powerset A x ↔ ↑x ⊆ A

@[simp]

theorem Class.sUnion_apply {x : Class} {y : ZFSet} :

(⋃₀ x) y ↔ ∃ (z : ZFSet), x z ∧ y ∈ z

@[simp]

theorem Class.coe_sUnion (x : ZFSet) :

↑(⋃₀ x) = ⋃₀ ↑x

@[simp]

theorem Class.mem_sUnion {x : Class} {y : Class} :

y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z

theorem Class.sInter_apply {x : Class} {y : ZFSet} :

(⋂₀ x) y ↔ ∀ (z : ZFSet), x z → y ∈ z

@[simp]

theorem Class.coe_sInter {x : ZFSet} (h : ZFSet.Nonempty x) :

↑(⋂₀ x) = ⋂₀ ↑x

theorem Class.mem_of_mem_sInter {x : Class} {y : Class} {z : Class} (hy : y ∈ ⋂₀ x) (hz : z ∈ x) :

y ∈ z

theorem Class.mem_sInter {x : Class} {y : Class} (h : Set.Nonempty x) :

y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

@[simp]

theorem Class.sUnion_empty :

⋃₀ ∅ = ∅

@[simp]

theorem Class.sInter_empty :

⋂₀ ∅ = Class.univ

theorem Class.eq_univ_of_powerset_subset {A : Class} (hA : Class.powerset A ⊆ A) :

A = Class.univ

An induction principle for sets. If every subset of a class is a member, then the class is universal.

def Class.iota (A : Class) :

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

Equations

Class.iota A = ⋃₀ {x : ZFSet | ∀ (y : ZFSet), A y ↔ y = x}

Instances For

theorem Class.iota_val (A : Class) (x : ZFSet) (H : ∀ (y : ZFSet), A y ↔ y = x) :

Class.iota A = ↑x

theorem Class.iota_ex (A : Class) :

Class.iota A ∈ 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 Class → Set function.

def Class.fval (F : Class) (A : Class) :