Analysis I, Section 3.1

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

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, 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.toObject of a Chapter3.Set X to make into a Chapter3.Object: this is mostly needed when manipulating sets 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 any sort of 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.)

class Chapter3.SetTheory : Type 1

Some of the axioms of Zermelo-Frankel theory with atoms

• Set : Type
• Object : Type
• set_to_object : Set ↪ Object
• mem : Object → Set → Prop
• emptyset : Set
• emptyset_mem (x : Object) : ¬mem x emptyset
• extensionality (X Y : Set) : (∀ (x : Object), mem x X ↔ mem x Y) → X = Y
• 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 }

instance Chapter3.objects_mem_sets [SetTheory] : Membership Object Set

Definition 3.1.1 (objects can be elements of sets)

Equations

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

instance Chapter3.sets_are_objects [SetTheory] : Coe Set Object

Axiom 3.1 (Sets are objects)

Equations

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

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.toObject [SetTheory] (X : Set) : Object

Equations

• X.toObject = Chapter3.SetTheory.set_to_object X

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

Axiom 3.1 (Sets are objects)

@[simp]

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

Axiom 3.1 (Sets are objects)

@[reducible, inline]

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

Axiom 3.2 (Equality of sets)

Equations

• ⋯ = ⋯

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

Axiom 3.2 (Equality of sets)

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

Equations

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

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

Axiom 3.3 (empty set). Note: 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 is unique

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)

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

Equations

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

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

Axiom 3.3(a) (singleton). Note 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 }

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 }

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

Axiom 3.3(b) (pair). Note that one often has to cast {a,b} to Set

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

Axiom 3.3(b) (pair). Note that one often has to cast {a,b} to Set

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

Remark 3.1.8

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

Remark 3.1.8

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

Remark 3.1.8

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

Remark 3.1.8

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.empty.toObject}

@[reducible, inline]

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

Equations

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

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

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

Proposition 3.1.27(c)

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

Proposition 3.1.27(a)

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.uinstSubset [SetTheory] : HasSubset Set

Definition 3.1.14.

Equations

• Chapter3.SetTheory.Set.uinstSubset = { 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

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

Examples 3.1.16

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

This defines the subtype A.toSubtype for any A:Set. 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

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⟩

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)

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 }

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 }

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)

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} (hAX : A ⊆ X) : A ∩ (X \ A) = ∅

Proposition 3.1.27(f)

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

Proposition 3.1.27(g)

theorem Chapter3.SetTheory.Set.compl_inter [SetTheory] {A B X : Set} (hAX : A ⊆ X) (hBX : B ⊆ X) : 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

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

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

theorem Chapter3.SetTheory.Set.subset_tfae [SetTheory] (A B C : 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

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

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

Exercise 3.1.7

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

Exercise 3.1.8

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.Set.pairwise_disjoint [SetTheory] (A B : Set) : Pairwise (Function.onFun Disjoint ![A \ B, A ∩ B, B \ A])

Exercise 3.1.10

theorem Chapter3.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 : Set), A ⊆ B ∧ ∀ (x : A.toSubtype), ↑x ∈ B ↔ P x

Exercise 3.1.11. The challenge is to prove this without using Set.specify, Set.specification_axiom, or Set.specification_axiom'.

theorem Chapter3.SetTheory.Set.subset_union_subset [SetTheory] {A B A' B' : Set} (hA'A : A' ⊆ A) (hB'B : B' ⊆ B) : A ∪ A' ⊆ 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 ∩ A' ⊆ 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 \ A' ⊆ B ∩ B'

Exercise 3.1.12.

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

Exercise 3.1.13