Analysis I, Section 3.1: Fundamentals (of set theory)

In this section we set up a version of Zermelo-Frankel set theory (with atoms) that tries to be as faithful as possible to the original text of Analysis I, Section 3.1. All numbering refers to the original text.

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• A type Chapter3.SetTheory.Set of sets
• A type Chapter3.SetTheory.Object of objects
• An axiom that every set is (or can be coerced into) an object
• The empty set ∅, singletons {y}, and pairs {y,z} (and more general finite tuples), with their attendant axioms
• Pairwise union X ∪ Y, and their attendant axioms
• Coercion of a set A to its associated type A.toSubtype, which is a subtype of Object, and basic API. (This is a technical construction needed to make the Zermelo-Frankel set theory compatible with the dependent type theory of Lean.)
• The specification A.specify P of a set A and a predicate P: A.toSubtype → Prop to the subset of elements of A obeying P, and the axiom of specification. TODO: somehow implement set builder elaboration for this.
• The replacement A.replace hP of a set A via a predicate P: A.toSubtype → Object → Prop obeying a uniqueness condition ∀ x y y', P x y ∧ P x y' → y = y', and the axiom of replacement.
• A bijective correspondence between the Mathlib natural numbers ℕ and a set Chapter3.Nat : Chapter3.Set (the axiom of infinity).
• Axioms of regularity, power set, and union (used in later sections of this chapter, but not required here)
• Connections with Mathlib's notion of a set

The other axioms of Zermelo-Frankel set theory are discussed in later sections.

Some technical notes:

• Mathlib of course has its own notion of a Set (or more precisely, a type Set X associated to each type X), which is not compatible with the notion Chapter3.Set defined here, though we will try to make the notations match as much as possible. This causes some notational conflict: for instance, one may need to explicitly specify (∅:Chapter3.Set) instead of just ∅ to indicate that one is using the Chapter3.Set version of the empty set, rather than the Mathlib version of the empty set, and similarly for other notation defined here.
• In Analysis I, we chose to work with an "impure" set theory, in which there could be more Objects than just Sets. In the type theory of Lean, this requires treating Chapter3.Set and Chapter3.Object as distinct types. Occasionally this means we have to use a coercion (X: Chapter3.Object) of a Chapter3.Set X to make into a Chapter3.Object: this is mostly needed when manipulating sets of sets.
• Strictly speaking, a set X:Set is not a type; however, we will coerce sets to types, and specifically to a subtype of Object. A similar coercion is in place for Mathlib's formalization of sets.
• After this chapter is concluded, the notion of a Chapter3.SetTheory.Set will be deprecated in favor of the standard Mathlib notion of a Set (or more precisely of the type Set X of a set in a given type X). However, due to various technical incompatibilities between set theory and type theory, we will not attempt to create a full equivalence between these two notions of sets. (As such, this makes this entire chapter optional from the point of view of the rest of the book, though we retain it for pedagogical purposes.)

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

• (Add tip here)

class Chapter3.SetTheory : Type (max (u + 1) (v + 1))

The axioms of Zermelo-Frankel theory with atoms.

• Set : Type u
• Object : Type v
• set_to_object : Set ↪ Object
• mem : Object → Set → Prop
• extensionality (X Y : Set) : (∀ (x : Object), mem x X ↔ mem x Y) → X = Y
• emptyset : Set
• emptyset_mem (x : Object) : ¬mem x emptyset
• singleton : Object → Set
• singleton_axiom (x y : Object) : mem x (singleton y) ↔ x = y
• union_pair : Set → Set → Set
• union_pair_axiom (X Y : Set) (x : Object) : mem x (union_pair X Y) ↔ mem x X ∨ mem x Y
• specify (A : Set) (P : { x : Object // mem x A } → Prop) : Set
• specification_axiom (A : Set) (P : { x : Object // mem x A } → Prop) : (∀ (x : Object), mem x (specify A P) → mem x A) ∧ ∀ (x : { x : Object // mem x A }), mem (↑x) (specify A P) ↔ P x
• replace (A : Set) (P : { x : Object // mem x A } → Object → Prop) (hP : ∀ (x : { x : Object // mem x A }) (y y' : Object), P x y ∧ P x y' → y = y') : Set
• replacement_axiom (A : Set) (P : { x : Object // mem x A } → Object → Prop) (hP : ∀ (x : { x : Object // mem x A }) (y y' : Object), P x y ∧ P x y' → y = y') (y : Object) : mem y (replace A P hP) ↔ ∃ (x : { x : Object // mem x A }), P x y
• nat : Set
• nat_equiv : ℕ ≃ { x : Object // mem x nat }
• regularity_axiom (A : Set) (hA : ∃ (x : Object), mem x A) : ∃ (x : Object), mem x A ∧ ∀ (S : Set), x = set_to_object S → ¬∃ (y : Object), mem y A ∧ mem y S
• pow : Set → Set → Set
• function_to_object (X Y : Set) : ({ x : Object // mem x X } → { x : Object // mem x Y }) ↪ Object
• powerset_axiom (X Y : Set) (F : Object) : mem F (pow X Y) ↔ ∃ (f : { x : Object // mem x Y } → { x : Object // mem x X }), (function_to_object Y X) f = F
• union : Set → Set
• union_axiom (A : Set) (x : Object) : mem x (union A) ↔ ∃ (S : Set), mem x S ∧ mem (set_to_object S) A

instance Chapter3.SetTheory.objects_mem_sets [SetTheory] : Membership Object Set

Definition 3.1.1 (objects can be elements of sets)

Equations

• Chapter3.SetTheory.objects_mem_sets = { mem := fun (X : Chapter3.Set) (x : Chapter3.Object) => Chapter3.SetTheory.mem x X }

instance Chapter3.SetTheory.sets_are_objects [SetTheory] : Coe Set Object

Axiom 3.1 (Sets are objects)

Equations

• Chapter3.SetTheory.sets_are_objects = { coe := fun (X : Chapter3.Set) => Chapter3.SetTheory.set_to_object X }

theorem Chapter3.SetTheory.Set.coe_eq [SetTheory] {X Y : Set} (h : set_to_object X = set_to_object Y) : X = Y

Axiom 3.1 (Sets are objects)

@[simp]

theorem Chapter3.SetTheory.Set.coe_eq_iff [SetTheory] (X Y : Set) : set_to_object X = set_to_object Y ↔ X = Y

Axiom 3.1 (Sets are objects)

theorem Chapter3.SetTheory.Set.ext [SetTheory] {X Y : Set} (h : ∀ (x : Object), x ∈ X ↔ x ∈ Y) : X = Y

Axiom 3.2 (Equality of sets). The [ext] tag allows the ext tactic to work for sets.

theorem Chapter3.SetTheory.Set.ext_iff [SetTheory] {X Y : Set} : X = Y ↔ ∀ (x : Object), x ∈ X ↔ x ∈ Y

instance Chapter3.SetTheory.Set.instEmpty [SetTheory] : EmptyCollection Set

Equations

• Chapter3.SetTheory.Set.instEmpty = { emptyCollection := Chapter3.SetTheory.emptyset }

@[simp]

theorem Chapter3.SetTheory.Set.not_mem_empty [SetTheory] (x : Object) : x ∉ ∅

Axiom 3.3 (empty set). Note: in some applications one may have to explicitly cast ∅ to Set due to Mathlib's existing set theory notation.

theorem Chapter3.SetTheory.Set.eq_empty_iff_forall_notMem [SetTheory] {X : Set} : X = ∅ ↔ ∀ (x : Object), x ∉ X

Empty set has no elements

theorem Chapter3.SetTheory.Set.empty_unique [SetTheory] : ∃! X : Set, ∀ (x : Object), x ∉ X

Empty set is unique

theorem Chapter3.SetTheory.Set.nonempty_def [SetTheory] {X : Set} (h : X ≠ ∅) : ∃ (x : Object), x ∈ X

Lemma 3.1.5 (Single choice)

theorem Chapter3.SetTheory.Set.nonempty_of_inhabited [SetTheory] {X : Set} {x : Object} (h : x ∈ X) : X ≠ ∅

instance Chapter3.SetTheory.Set.instSingleton [SetTheory] : Singleton Object Set

Equations

• Chapter3.SetTheory.Set.instSingleton = { singleton := Chapter3.SetTheory.singleton }

@[simp]

theorem Chapter3.SetTheory.Set.mem_singleton [SetTheory] (x a : Object) : x ∈ {a} ↔ x = a

Axiom 3.3(a) (singleton). Note: in some applications one may have to explicitly cast {a} to Set due to Mathlib's existing set theory notation.

instance Chapter3.SetTheory.Set.instUnion [SetTheory] : Union Set

Equations

• Chapter3.SetTheory.Set.instUnion = { union := Chapter3.SetTheory.union_pair }

@[simp]

theorem Chapter3.SetTheory.Set.mem_union [SetTheory] (x : Object) (X Y : Set) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y

Axiom 3.4 (Pairwise union)

instance Chapter3.SetTheory.Set.instInsert [SetTheory] : Insert Object Set

Equations

• Chapter3.SetTheory.Set.instInsert = { insert := fun (x : Chapter3.Object) (X : Chapter3.Set) => {x} ∪ X }

@[simp]

theorem Chapter3.SetTheory.Set.mem_insert [SetTheory] (a b : Object) (X : Set) : a ∈ insert b X ↔ a = b ∨ a ∈ X

theorem Chapter3.SetTheory.Set.pair_eq [SetTheory] (a b : Object) : {a, b} = {a} ∪ {b}

Axiom 3.3(b) (pair). Note: in some applications one may have to cast {a,b} to Set.

@[simp]

theorem Chapter3.SetTheory.Set.mem_pair [SetTheory] (x a b : Object) : x ∈ {a, b} ↔ x = a ∨ x = b

Axiom 3.3(b) (pair). Note: in some applications one may have to cast {a,b} to Set.

@[simp]

theorem Chapter3.SetTheory.Set.mem_triple [SetTheory] (x a b c : Object) : x ∈ {a, b, c} ↔ x = a ∨ x = b ∨ x = c

theorem Chapter3.SetTheory.Set.singleton_uniq [SetTheory] (a : Object) : ∃! X : Set, ∀ (x : Object), x ∈ X ↔ x = a

Remark 3.1.9

theorem Chapter3.SetTheory.Set.pair_uniq [SetTheory] (a b : Object) : ∃! X : Set, ∀ (x : Object), x ∈ X ↔ x = a ∨ x = b

Remark 3.1.9

theorem Chapter3.SetTheory.Set.pair_comm [SetTheory] (a b : Object) : {a, b} = {b, a}

Remark 3.1.9

@[simp]

theorem Chapter3.SetTheory.Set.pair_self [SetTheory] (a : Object) : {a, a} = {a}

Remark 3.1.9

theorem Chapter3.SetTheory.Set.pair_eq_pair [SetTheory] {a b c d : Object} (h : {a, b} = {c, d}) : a = c ∧ b = d ∨ a = d ∧ b = c

Exercise 3.1.1

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.empty [SetTheory] : Set

Equations

• Chapter3.SetTheory.Set.empty = ∅

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.singleton_empty [SetTheory] : Set

Equations

• Chapter3.SetTheory.Set.singleton_empty = {Chapter3.SetTheory.set_to_object Chapter3.SetTheory.Set.empty}

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.pair_empty [SetTheory] : Set

Equations

• Chapter3.SetTheory.Set.pair_empty = {Chapter3.SetTheory.set_to_object Chapter3.SetTheory.Set.empty, Chapter3.SetTheory.set_to_object Chapter3.SetTheory.Set.singleton_empty}

theorem Chapter3.SetTheory.Set.emptyset_neq_singleton [SetTheory] : empty ≠ singleton_empty

Exercise 3.1.2

theorem Chapter3.SetTheory.Set.emptyset_neq_pair [SetTheory] : empty ≠ pair_empty

Exercise 3.1.2

theorem Chapter3.SetTheory.Set.singleton_empty_neq_pair [SetTheory] : singleton_empty ≠ pair_empty

Exercise 3.1.2

theorem Chapter3.SetTheory.Set.union_congr_left [SetTheory] (A A' B : Set) (h : A = A') : A ∪ B = A' ∪ B

Remark 3.1.11. (These results can be proven either by a direct rewrite, or by using extensionality.)

theorem Chapter3.SetTheory.Set.union_congr_right [SetTheory] (A B B' : Set) (h : B = B') : A ∪ B = A ∪ B'

Remark 3.1.11. (These results can be proven either by a direct rewrite, or by using extensionality.)

theorem Chapter3.SetTheory.Set.singleton_union_singleton [SetTheory] (a b : Object) : {a} ∪ {b} = {a, b}

Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3

theorem Chapter3.SetTheory.Set.union_comm [SetTheory] (A B : Set) : A ∪ B = B ∪ A

Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3

theorem Chapter3.SetTheory.Set.union_assoc [SetTheory] (A B C : Set) : A ∪ B ∪ C = A ∪ (B ∪ C)

Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3

@[simp]

theorem Chapter3.SetTheory.Set.union_self [SetTheory] (A : Set) : A ∪ A = A

Proposition 3.1.27(c)

@[simp]

theorem Chapter3.SetTheory.Set.union_empty [SetTheory] (A : Set) : A ∪ ∅ = A

Proposition 3.1.27(a)

@[simp]

theorem Chapter3.SetTheory.Set.empty_union [SetTheory] (A : Set) : ∅ ∪ A = A

Proposition 3.1.27(a)

theorem Chapter3.SetTheory.Set.triple_eq [SetTheory] (a b c : Object) : {a, b, c} = {a} ∪ {b, c}

theorem Chapter3.SetTheory.Set.pair_union_pair [SetTheory] (a b c : Object) : {a, b} ∪ {b, c} = {a, b, c}

Example 3.1.10

instance Chapter3.SetTheory.Set.instSubset [SetTheory] : HasSubset Set

Definition 3.1.14.

Equations

• Chapter3.SetTheory.Set.instSubset = { Subset := fun (X Y : Chapter3.Set) => ∀ x ∈ X, x ∈ Y }

instance Chapter3.SetTheory.Set.instSSubset [SetTheory] : HasSSubset Set

Definition 3.1.14. Note that the strict subset operation in Mathlib is denoted ⊂ rather than ⊊.

Equations

• Chapter3.SetTheory.Set.instSSubset = { SSubset := fun (X Y : Chapter3.Set) => X ⊆ Y ∧ X ≠ Y }

theorem Chapter3.SetTheory.Set.subset_def [SetTheory] (X Y : Set) : X ⊆ Y ↔ ∀ x ∈ X, x ∈ Y

Definition 3.1.14.

theorem Chapter3.SetTheory.Set.ssubset_def [SetTheory] (X Y : Set) : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y

Definition 3.1.14. Note that the strict subset operation in Mathlib is denoted ⊂ rather than ⊊.

theorem Chapter3.SetTheory.Set.subset_congr_left [SetTheory] {A A' B : Set} (hAA' : A = A') (hAB : A ⊆ B) : A' ⊆ B

Remark 3.1.15

@[simp]

theorem Chapter3.SetTheory.Set.subset_self [SetTheory] (A : Set) : A ⊆ A

Examples 3.1.16

@[simp]

theorem Chapter3.SetTheory.Set.empty_subset [SetTheory] (A : Set) : ∅ ⊆ A

Examples 3.1.16

theorem Chapter3.SetTheory.Set.subset_trans [SetTheory] {A B C : Set} (hAB : A ⊆ B) (hBC : B ⊆ C) : A ⊆ C

Proposition 3.1.17 (Partial ordering by set inclusion)

theorem Chapter3.SetTheory.Set.subset_antisymm [SetTheory] (A B : Set) (hAB : A ⊆ B) (hBA : B ⊆ A) : A = B

Proposition 3.1.17 (Partial ordering by set inclusion)

theorem Chapter3.SetTheory.Set.ssubset_trans [SetTheory] (A B C : Set) (hAB : A ⊂ B) (hBC : B ⊂ C) : A ⊂ C

Proposition 3.1.17 (Partial ordering by set inclusion)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.toSubtype [SetTheory] (A : Set) : Type u_2

This defines the subtype A.toSubtype for any A:Set. Note that A.toSubtype gives you a type, similar to how Object or Set are types. A value x' of type A.toSubtype combines some x: Object with a proof that hx: x ∈ A.

To produce an element x' of this subtype, use ⟨ x, hx ⟩, where x: Object and hx: x ∈ A. The object x associated to a subtype element x' is recovered as x'.val, and the property hx that x belongs to A is recovered as x'.property.

Equations

• A.toSubtype = { x : Chapter3.Object // x ∈ A }

instance Chapter3.instCoeSortSetType [SetTheory] : CoeSort Set (Type v)

Equations

• Chapter3.instCoeSortSetType = { coe := fun (A : Chapter3.Set) => A.toSubtype }

theorem Chapter3.SetTheory.Set.subtype_property [SetTheory] (A : Set) (x : A.toSubtype) : ↑x ∈ A

Elements of a set (implicitly coerced to a subtype) are also elements of the set (with respect to the membership operation of the set theory).

theorem Chapter3.SetTheory.Set.subtype_coe [SetTheory] (A : Set) (x : A.toSubtype) : ↑x = ↑x

theorem Chapter3.SetTheory.Set.coe_inj [SetTheory] (A : Set) (x y : A.toSubtype) : ↑x = ↑y ↔ x = y

def Chapter3.SetTheory.Set.subtype_mk [SetTheory] (A : Set) {x : Object} (hx : x ∈ A) : A.toSubtype

If one has a proof hx of x ∈ A, then A.subtype_mk hx will then make the element of A (viewed as a subtype) corresponding to x.

Equations

• A.subtype_mk hx = ⟨x, hx⟩

@[simp]

theorem Chapter3.SetTheory.Set.subtype_mk_coe [SetTheory] {A : Set} {x : Object} (hx : x ∈ A) : ↑(A.subtype_mk hx) = x

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.specify [SetTheory] (A : Set) (P : A.toSubtype → Prop) : Set

Equations

• A.specify P = Chapter3.SetTheory.specify A P

theorem Chapter3.SetTheory.Set.specification_axiom [SetTheory] {A : Set} {P : A.toSubtype → Prop} {x : Object} (h : x ∈ A.specify P) : x ∈ A

Axiom 3.6 (axiom of specification)

theorem Chapter3.SetTheory.Set.specification_axiom' [SetTheory] {A : Set} (P : A.toSubtype → Prop) (x : A.toSubtype) : ↑x ∈ A.specify P ↔ P x

Axiom 3.6 (axiom of specification)

@[simp]

theorem Chapter3.SetTheory.Set.specification_axiom'' [SetTheory] {A : Set} (P : A.toSubtype → Prop) (x : Object) : x ∈ A.specify P ↔ ∃ (h : x ∈ A), P ⟨x, h⟩

Axiom 3.6 (axiom of specification)

theorem Chapter3.SetTheory.Set.specify_subset [SetTheory] {A : Set} (P : A.toSubtype → Prop) : A.specify P ⊆ A

theorem Chapter3.SetTheory.Set.specify_congr [SetTheory] {A A' : Set} (hAA' : A = A') {P : A.toSubtype → Prop} {P' : A'.toSubtype → Prop} (hPP' : ∀ (x : Object) (h : x ∈ A) (h' : x ∈ A'), P ⟨x, h⟩ ↔ P' ⟨x, h'⟩) : A.specify P = A'.specify P'

This exercise may require some understanding of how subtypes are implemented in Lean.

instance Chapter3.SetTheory.Set.instIntersection [SetTheory] : Inter Set

Equations

• Chapter3.SetTheory.Set.instIntersection = { inter := fun (X Y : Chapter3.Set) => X.specify fun (x : X.toSubtype) => ↑x ∈ Y }

@[simp]

theorem Chapter3.SetTheory.Set.mem_inter [SetTheory] (x : Object) (X Y : Set) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y

Definition 3.1.22 (Intersections)

instance Chapter3.SetTheory.Set.instSDiff [SetTheory] : SDiff Set

Equations

• Chapter3.SetTheory.Set.instSDiff = { sdiff := fun (X Y : Chapter3.Set) => X.specify fun (x : X.toSubtype) => ↑x ∉ Y }

@[simp]

theorem Chapter3.SetTheory.Set.mem_sdiff [SetTheory] (x : Object) (X Y : Set) : x ∈ X \ Y ↔ x ∈ X ∧ x ∉ Y

Definition 3.1.26 (Difference sets)

theorem Chapter3.SetTheory.Set.inter_comm [SetTheory] (A B : Set) : A ∩ B = B ∩ A

Proposition 3.1.27(d) / Exercise 3.1.6

theorem Chapter3.SetTheory.Set.subset_union [SetTheory] {A X : Set} (hAX : A ⊆ X) : A ∪ X = X

Proposition 3.1.27(b)

theorem Chapter3.SetTheory.Set.union_subset [SetTheory] {A X : Set} (hAX : A ⊆ X) : X ∪ A = X

Proposition 3.1.27(b)

@[simp]

theorem Chapter3.SetTheory.Set.inter_self [SetTheory] (A : Set) : A ∩ A = A

Proposition 3.1.27(c)

theorem Chapter3.SetTheory.Set.inter_assoc [SetTheory] (A B C : Set) : A ∩ B ∩ C = A ∩ (B ∩ C)

Proposition 3.1.27(e)

theorem Chapter3.SetTheory.Set.inter_union_distrib_left [SetTheory] (A B C : Set) : A ∩ (B ∪ C) = A ∩ B ∪ A ∩ C

Proposition 3.1.27(f)

theorem Chapter3.SetTheory.Set.union_inter_distrib_left [SetTheory] (A B C : Set) : A ∪ B ∩ C = (A ∪ B) ∩ (A ∪ C)

Proposition 3.1.27(f)

theorem Chapter3.SetTheory.Set.union_compl [SetTheory] {A X : Set} (hAX : A ⊆ X) : A ∪ X \ A = X

Proposition 3.1.27(f)

theorem Chapter3.SetTheory.Set.inter_compl [SetTheory] {A X : Set} : A ∩ (X \ A) = ∅

Proposition 3.1.27(f)

theorem Chapter3.SetTheory.Set.compl_union [SetTheory] {A B X : Set} : X \ (A ∪ B) = X \ A ∩ (X \ B)

Proposition 3.1.27(g)

theorem Chapter3.SetTheory.Set.compl_inter [SetTheory] {A B X : Set} : X \ (A ∩ B) = X \ A ∪ X \ B

Proposition 3.1.27(g)

instance Chapter3.SetTheory.Set.instDistribLattice [SetTheory] : DistribLattice Set

Not from textbook: sets form a distributive lattice.

Equations

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

instance Chapter3.SetTheory.Set.instOrderBot [SetTheory] : OrderBot Set

Sets have a minimal element.

Equations

• Chapter3.SetTheory.Set.instOrderBot = { bot := ∅, bot_le := ⋯ }

theorem Chapter3.SetTheory.Set.disjoint_iff [SetTheory] (A B : Set) : Disjoint A B ↔ A ∩ B = ∅

Definition of disjointness (using the previous instances)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.replace [SetTheory] (A : Set) {P : A.toSubtype → Object → Prop} (hP : ∀ (x : A.toSubtype) (y y' : Object), P x y ∧ P x y' → y = y') : Set

Equations

• A.replace hP = Chapter3.SetTheory.replace A P hP

@[simp]

theorem Chapter3.SetTheory.Set.replacement_axiom [SetTheory] {A : Set} {P : A.toSubtype → Object → Prop} (hP : ∀ (x : A.toSubtype) (y y' : Object), P x y ∧ P x y' → y = y') (y : Object) : y ∈ A.replace hP ↔ ∃ (x : A.toSubtype), P x y

Axiom 3.7 (Axiom of replacement)

@[reducible, inline]

abbrev Chapter3.Nat [SetTheory] : Set

Equations

• Chapter3.Nat = Chapter3.SetTheory.nat

def Chapter3.SetTheory.Set.nat_equiv [SetTheory] : ℕ ≃ Nat.toSubtype

Axiom 3.8 (Axiom of infinity)

Equations

• Chapter3.SetTheory.Set.nat_equiv = Chapter3.SetTheory.nat_equiv

instance Chapter3.SetTheory.Set.instOfNat [SetTheory] {n : ℕ} : OfNat Nat.toSubtype n

Equations

• Chapter3.SetTheory.Set.instOfNat = { ofNat := Chapter3.SetTheory.Set.nat_equiv n }

instance Chapter3.SetTheory.Set.instNatCast [SetTheory] : NatCast Nat.toSubtype

Equations

• Chapter3.SetTheory.Set.instNatCast = { natCast := fun (n : ℕ) => Chapter3.SetTheory.Set.nat_equiv n }

instance Chapter3.SetTheory.Set.toNat [SetTheory] : Coe Nat.toSubtype ℕ

Equations

• Chapter3.SetTheory.Set.toNat = { coe := fun (n : Chapter3.Nat.toSubtype) => Chapter3.SetTheory.Set.nat_equiv.symm n }

instance Chapter3.SetTheory.Object.instNatCast [SetTheory] : NatCast Object

Equations

• Chapter3.SetTheory.Object.instNatCast = { natCast := fun (n : ℕ) => ↑↑n }

instance Chapter3.SetTheory.Object.instOfNat [SetTheory] {n : ℕ} : OfNat Object n

Equations

• Chapter3.SetTheory.Object.instOfNat = { ofNat := ↑↑n }

@[simp]

theorem Chapter3.SetTheory.Object.ofnat_eq [SetTheory] {n : ℕ} : ↑↑n = ↑n

theorem Chapter3.SetTheory.Object.ofnat_eq' [SetTheory] {n : ℕ} : OfNat.ofNat n = ↑n

@[simp]

theorem Chapter3.SetTheory.Object.ofnat_eq'' [SetTheory] {n : Nat.toSubtype} : ↑(Set.nat_equiv.symm n) = ↑n

@[simp]

theorem Chapter3.SetTheory.Object.ofnat_eq''' [SetTheory] {n : ℕ} {hn : ↑n ∈ nat} : Set.nat_equiv.symm ⟨↑n, hn⟩ = n

theorem Chapter3.SetTheory.Set.nat_coe_eq [SetTheory] {n : ℕ} : ↑n = OfNat.ofNat n

@[simp]

theorem Chapter3.SetTheory.Set.nat_equiv_inj [SetTheory] (n m : ℕ) : ↑n = ↑m ↔ n = m

@[simp]

theorem Chapter3.SetTheory.Set.nat_equiv_symm_inj [SetTheory] (n m : Nat.toSubtype) : nat_equiv.symm n = nat_equiv.symm m ↔ n = m

@[simp]

theorem Chapter3.SetTheory.Set.ofNat_inj [SetTheory] (n m : ℕ) : OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m

@[simp]

theorem Chapter3.SetTheory.Set.ofNat_inj' [SetTheory] (n m : ℕ) : OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m

@[simp]

theorem Chapter3.SetTheory.Set.nat_coe_eq_iff [SetTheory] {m n : ℕ} : ↑m = OfNat.ofNat n ↔ m = n

@[simp]

theorem Chapter3.SetTheory.Object.natCast_inj [SetTheory] (n m : ℕ) : ↑n = ↑m ↔ n = m

@[simp]

theorem Chapter3.SetTheory.Set.nat_equiv_coe_of_coe [SetTheory] (n : ℕ) : nat_equiv.symm ↑n = n

@[simp]

theorem Chapter3.SetTheory.Set.nat_equiv_coe_of_coe' [SetTheory] (n : Nat.toSubtype) : ↑(nat_equiv.symm n) = n

@[simp]

theorem Chapter3.SetTheory.Set.nat_equiv_coe_of_coe'' [SetTheory] (n : ℕ) : nat_equiv.symm (OfNat.ofNat n) = n

@[simp]

theorem Chapter3.SetTheory.Set.nat_coe_eq_iff' [SetTheory] {m : Nat.toSubtype} {n : ℕ} : ↑m = OfNat.ofNat n ↔ nat_equiv.symm m = OfNat.ofNat n

theorem Chapter3.SetTheory.Set.subset_tfae [SetTheory] (A B : Set) : [A ⊆ B, A ∪ B = B, A ∩ B = A].TFAE

Exercise 3.1.5. One can use the tfae_have and tfae_finish tactics here.

theorem Chapter3.SetTheory.Set.inter_subset_left [SetTheory] (A B : Set) : A ∩ B ⊆ A

Exercise 3.1.7

theorem Chapter3.SetTheory.Set.inter_subset_right [SetTheory] (A B : Set) : A ∩ B ⊆ B

Exercise 3.1.7

@[simp]

theorem Chapter3.SetTheory.Set.subset_inter_iff [SetTheory] (A B C : Set) : C ⊆ A ∩ B ↔ C ⊆ A ∧ C ⊆ B

Exercise 3.1.7

theorem Chapter3.SetTheory.Set.subset_union_left [SetTheory] (A B : Set) : A ⊆ A ∪ B

Exercise 3.1.7

theorem Chapter3.SetTheory.Set.subset_union_right [SetTheory] (A B : Set) : B ⊆ A ∪ B

Exercise 3.1.7

@[simp]

theorem Chapter3.SetTheory.Set.union_subset_iff [SetTheory] (A B C : Set) : A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C

Exercise 3.1.7

@[simp]

theorem Chapter3.SetTheory.Set.inter_union_cancel [SetTheory] (A B : Set) : A ∩ (A ∪ B) = A

Exercise 3.1.8

@[simp]

theorem Chapter3.SetTheory.Set.union_inter_cancel [SetTheory] (A B : Set) : A ∪ A ∩ B = A

Exercise 3.1.8

theorem Chapter3.SetTheory.Set.partition_left [SetTheory] {A B X : Set} (h_union : A ∪ B = X) (h_inter : A ∩ B = ∅) : A = X \ B

Exercise 3.1.9

theorem Chapter3.SetTheory.Set.partition_right [SetTheory] {A B X : Set} (h_union : A ∪ B = X) (h_inter : A ∩ B = ∅) : B = X \ A

Exercise 3.1.9

theorem Chapter3.SetTheory.Set.pairwise_disjoint [SetTheory] (A B : Set) : Pairwise (Function.onFun Disjoint ![A \ B, A ∩ B, B \ A])

Exercise 3.1.10. You may find Function.onFun_apply and the fin_cases tactic useful.

theorem Chapter3.SetTheory.Set.union_eq_partition [SetTheory] (A B : Set) : A ∪ B = A \ B ∪ A ∩ B ∪ B \ A

Exercise 3.1.10

theorem Chapter3.SetTheory.Set.specification_from_replacement [SetTheory] {A : Set} {P : A.toSubtype → Prop} : ∃ B ⊆ A, ∀ (x : A.toSubtype), ↑x ∈ B ↔ P x

Exercise 3.1.11. The challenge is to prove this without using Set.specify, Set.specification_axiom, Set.specification_axiom', or anything built from them (like differences and intersections).

theorem Chapter3.SetTheory.Set.subset_union_subset [SetTheory] {A B A' B' : Set} (hA'A : A' ⊆ A) (hB'B : B' ⊆ B) : A' ∪ B' ⊆ A ∪ B

Exercise 3.1.12.

theorem Chapter3.SetTheory.Set.subset_inter_subset [SetTheory] {A B A' B' : Set} (hA'A : A' ⊆ A) (hB'B : B' ⊆ B) : A' ∩ B' ⊆ A ∩ B

Exercise 3.1.12.

theorem Chapter3.SetTheory.Set.subset_diff_subset_counter [SetTheory] : ∃ (A : Set) (B : Set) (A' : Set) (B' : Set), A' ⊆ A ∧ B' ⊆ B ∧ ¬A' \ B' ⊆ A \ B

Exercise 3.1.12.

theorem Chapter3.SetTheory.Set.singleton_iff [SetTheory] (A : Set) (hA : A ≠ ∅) : (¬∃ B ⊂ A, B ≠ ∅) ↔ ∃ (x : Object), A = {x}

Exercise 3.1.13

instance Chapter3.SetTheory.Set.inst_coe_set [SetTheory] : Coe Set (_root_.Set Object)

Equations

• Chapter3.SetTheory.Set.inst_coe_set = { coe := fun (X : Chapter3.Set) => {x : Chapter3.Object | x ∈ X} }

@[simp]

theorem Chapter3.SetTheory.Set.coe_inj' [SetTheory] (X Y : Set) : {x : Object | x ∈ X} = {x : Object | x ∈ Y} ↔ X = Y

Injectivity of the coercion. Note however that we do NOT assert that the coercion is surjective (and indeed Russell's paradox prevents this)

theorem Chapter3.SetTheory.Set.mem_coe [SetTheory] (X : Set) (x : Object) : x ∈ {x : Object | x ∈ X} ↔ x ∈ X

Compatibility of the membership operation ∈

theorem Chapter3.SetTheory.Set.coe_empty [SetTheory] : {x : Object | x ∈ ∅} = ∅

Compatibility of the emptyset

theorem Chapter3.SetTheory.Set.coe_subset [SetTheory] (X Y : Set) : {x : Object | x ∈ X} ⊆ {x : Object | x ∈ Y} ↔ X ⊆ Y

Compatibility of subset

theorem Chapter3.SetTheory.Set.coe_ssubset [SetTheory] (X Y : Set) : {x : Object | x ∈ X} ⊂ {x : Object | x ∈ Y} ↔ X ⊂ Y

theorem Chapter3.SetTheory.Set.coe_singleton [SetTheory] (x : Object) : {x} = {x}

Compatibility of singleton

theorem Chapter3.SetTheory.Set.coe_union [SetTheory] (X Y : Set) : {x : Object | x ∈ X} ∪ {x : Object | x ∈ Y} = {x : Object | x ∈ X} ∪ {x : Object | x ∈ Y}

Compatibility of union

theorem Chapter3.SetTheory.Set.coe_pair [SetTheory] (x y : Object) : {x, y} = {x, y}

Compatibility of pair

theorem Chapter3.SetTheory.Set.coe_subtype [SetTheory] (X : Set) : ↑{x : Object | x ∈ X} = X.toSubtype

Compatibility of subtype

theorem Chapter3.SetTheory.Set.coe_intersection [SetTheory] (X Y : Set) : {x : Object | x ∈ X} ∩ {x : Object | x ∈ Y} = {x : Object | x ∈ X} ∩ {x : Object | x ∈ Y}

Compatibility of intersection

theorem Chapter3.SetTheory.Set.coe_diff [SetTheory] (X Y : Set) : {x : Object | x ∈ X} \ {x : Object | x ∈ Y} = {x : Object | x ∈ X} \ {x : Object | x ∈ Y}

Compatibility of set difference

theorem Chapter3.SetTheory.Set.coe_Disjoint [SetTheory] (X Y : Set) : Disjoint {x : Object | x ∈ X} {x : Object | x ∈ Y} ↔ Disjoint X Y

Compatibility of disjointness