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

namespace Chapter3

Some of the axioms of Zermelo-Frankel theory with atoms

class SetTheory where Set : Type Object : Type set_to_object : Set ↪ Object mem : Object → Set → Prop emptyset: Set emptyset_mem x : ¬ mem x emptyset extensionality X Y : (∀ x, mem x X ↔ mem x Y) → X = Y singleton : Object → Set singleton_axiom x y : mem x (singleton y) ↔ x = y union_pair : Set → Set → Set union_pair_axiom X Y x : mem x (union_pair X Y) ↔ (mem x X ∨ mem x Y) specify A (P: Subtype (fun x ↦ mem x A) → Prop) : Set specification_axiom A (P: Subtype (fun x ↦ mem x A) → Prop) : (∀ x, mem x (specify A P) → mem x A) ∧ ∀ x, mem x.val (specify A P) ↔ P x replace A (P: Subtype (fun x ↦ mem x A) → Object → Prop) (hP: ∀ x y y', P x y ∧ P x y' → y = y') : Set replacement_axiom A (P: Subtype (fun x ↦ mem x A) → Object → Prop) (hP: ∀ x y y', P x y ∧ P x y' → y = y') : ∀ y, mem y (replace A P hP) ↔ ∃ x, P x y nat : Set nat_equiv : ℕ ≃ Subtype (fun x ↦ mem x nat)export SetTheory (Set Object)-- This instance implicitly imposes (some of) the axioms of Zermelo-Frankel set theory with atoms. variable [SetTheory]

Definition 3.1.1 (objects can be elements of sets)

instance objects_mem_sets : Membership Object Set where mem X x := SetTheory.mem x X

Axiom 3.1 (Sets are objects)

instance sets_are_objects : Coe Set Object where coe X := SetTheory.set_to_object Xabbrev SetTheory.Set.toObject (X:Set) : Object := X

Axiom 3.1 (Sets are objects)

theorem SetTheory.Set.coe_eq {X Y:Set} (h: X.toObject = Y.toObject) : X = Y := SetTheory.set_to_object.inj' h

Axiom 3.1 (Sets are objects)

@[simp] theorem SetTheory.Set.coe_eq_iff (X Y:Set) : X.toObject = Y.toObject ↔ X = Y := byinst✝:SetTheoryX:SetY:Set⊢ X.toObject = Y.toObject ↔ X = Y constructormpinst✝:SetTheoryX:SetY:Set⊢ X.toObject = Y.toObject → X = Ymprinst✝:SetTheoryX:SetY:Set⊢ X = Y → X.toObject = Y.toObject .mpinst✝:SetTheoryX:SetY:Set⊢ X.toObject = Y.toObject → X = Y exact coe_eqAll goals completed! 🐙 intro hmprinst✝:SetTheoryX:SetY:Seth:X = Y⊢ X.toObject = Y.toObject; subst hmprinst✝:SetTheoryX:Set⊢ X.toObject = X.toObject; rflAll goals completed! 🐙

Axiom 3.2 (Equality of sets)

abbrev SetTheory.Set.ext {X Y:Set} (h: ∀ x, x ∈ X ↔ x ∈ Y) : X = Y := SetTheory.extensionality _ _ h

Axiom 3.2 (Equality of sets)

theorem SetTheory.Set.ext_iff (X Y: Set) : X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y := byinst✝:SetTheoryX:SetY:Set⊢ X = Y ↔ ∀ (x : Object), x ∈ X ↔ x ∈ Y constructormpinst✝:SetTheoryX:SetY:Set⊢ X = Y → ∀ (x : Object), x ∈ X ↔ x ∈ Ymprinst✝:SetTheoryX:SetY:Set⊢ (∀ (x : Object), x ∈ X ↔ x ∈ Y) → X = Y .mpinst✝:SetTheoryX:SetY:Set⊢ X = Y → ∀ (x : Object), x ∈ X ↔ x ∈ Y intro hmpinst✝:SetTheoryX:SetY:Seth:X = Y⊢ ∀ (x : Object), x ∈ X ↔ x ∈ Y; subst hmpinst✝:SetTheoryX:Set⊢ ∀ (x : Object), x ∈ X ↔ x ∈ X; simpAll goals completed! 🐙 .mprinst✝:SetTheoryX:SetY:Set⊢ (∀ (x : Object), x ∈ X ↔ x ∈ Y) → X = Y intro hmprinst✝:SetTheoryX:SetY:Seth:∀ (x : Object), x ∈ X ↔ x ∈ Y⊢ X = Y; apply extmpr.hinst✝:SetTheoryX:SetY:Seth:∀ (x : Object), x ∈ X ↔ x ∈ Y⊢ ∀ (x : Object), x ∈ X ↔ x ∈ Y; exact hAll goals completed! 🐙instance SetTheory.Set.instEmpty : EmptyCollection Set where emptyCollection := SetTheory.emptyset

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

theorem SetTheory.Set.not_mem_empty : ∀ x, x ∉ (∅:Set) := SetTheory.emptyset_mem

Empty set is unique

theorem declaration uses 'sorry'SetTheory.Set.eq_empty_iff_forall_notMem {X:Set} : X = ∅ ↔ (∀ x, ¬ x ∈ X) := byinst✝:SetTheoryX:Set⊢ X = ∅ ↔ ∀ (x : Object), x ∉ X sorryAll goals completed! 🐙

Empty set is unique

theorem declaration uses 'sorry'SetTheory.Set.empty_unique : ∃! (X:Set), ∀ x, ¬ x ∈ X := byinst✝:SetTheory⊢ ∃! X, ∀ (x : Object), x ∉ X sorryAll goals completed! 🐙/-- Lemma 3.1.5 (Single choice) -/ lemma SetTheory.Set.nonempty_def {X:Set} (h: X ≠ ∅) : ∃ x, x ∈ X := byinst✝:SetTheoryX:Seth:X ≠ ∅⊢ ∃ x, x ∈ X -- This proof is written to follow the structure of the original text. by_contra! thisinst✝:SetTheoryX:Seth:X ≠ ∅this:∀ (x : Object), x ∉ X⊢ False have claim (x:Object) : x ∈ X ↔ x ∈ (∅:Set) := byinst✝:SetTheoryX:Seth:X ≠ ∅⊢ ∃ x, x ∈ X simp [this, not_mem_empty]All goals completed! 🐙 replace claim := ext claiminst✝:SetTheoryX:Seth:X ≠ ∅this:∀ (x : Object), x ∉ Xclaim:X = ∅⊢ False contradictionAll goals completed! 🐙instance SetTheory.Set.instSingleton : Singleton Object Set where singleton := SetTheory.singleton

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

theorem SetTheory.Set.mem_singleton (x a:Object) : x ∈ ({a}:Set) ↔ x = a := byinst✝:SetTheoryx:Objecta:Object⊢ x ∈ {a} ↔ x = a exact SetTheory.singleton_axiom x aAll goals completed! 🐙instance SetTheory.Set.instUnion : Union Set where union := SetTheory.union_pair

Axiom 3.4 (Pairwise union)

theorem SetTheory.Set.mem_union (x:Object) (X Y:Set) : x ∈ (X ∪ Y) ↔ (x ∈ X ∨ x ∈ Y) := SetTheory.union_pair_axiom X Y xinstance SetTheory.Set.instInsert : Insert Object Set where insert x X := {x} ∪ X

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

theorem SetTheory.Set.pair_eq (a b:Object) : ({a,b}:Set) = {a} ∪ {b} := byinst✝:SetTheorya:Objectb:Object⊢ {a, b} = {a} ∪ {b} rflAll goals completed! 🐙

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

theorem SetTheory.Set.mem_pair (x a b:Object) : x ∈ ({a,b}:Set) ↔ (x = a ∨ x = b) := byinst✝:SetTheoryx:Objecta:Objectb:Object⊢ x ∈ {a, b} ↔ x = a ∨ x = b rw [pair_eq, mem_union, mem_singleton, mem_singleton]All goals completed! 🐙

Remark 3.1.8

theorem declaration uses 'sorry'SetTheory.Set.singleton_uniq (a:Object) : ∃! (X:Set), ∀ x, x ∈ X ↔ x = a := byinst✝:SetTheorya:Object⊢ ∃! X, ∀ (x : Object), x ∈ X ↔ x = a sorryAll goals completed! 🐙

Remark 3.1.8

theorem declaration uses 'sorry'SetTheory.Set.pair_uniq (a b:Object) : ∃! (X:Set), ∀ x, x ∈ X ↔ x = a ∨ x = b := byinst✝:SetTheorya:Objectb:Object⊢ ∃! X, ∀ (x : Object), x ∈ X ↔ x = a ∨ x = b sorryAll goals completed! 🐙

Remark 3.1.8

theorem declaration uses 'sorry'SetTheory.Set.pair_comm (a b:Object) : ({a,b}:Set) = {b,a} := byinst✝:SetTheorya:Objectb:Object⊢ {a, b} = {b, a} sorryAll goals completed! 🐙

Remark 3.1.8

theorem declaration uses 'sorry'SetTheory.Set.pair_self (a:Object) : ({a,a}:Set) = {a} := byinst✝:SetTheorya:Object⊢ {a, a} = {a} sorryAll goals completed! 🐙

Exercise 3.1.1

theorem declaration uses 'sorry'SetTheory.Set.pair_eq_pair {a b c d:Object} (h: ({a,b}:Set) = {c,d}) : a = c ∧ b = d ∨ a = d ∧ b = c := byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecth:{a, b} = {c, d}⊢ a = c ∧ b = d ∨ a = d ∧ b = c sorryAll goals completed! 🐙abbrev SetTheory.Set.empty : Set := ∅abbrev SetTheory.Set.singleton_empty : Set := {empty.toObject}abbrev SetTheory.Set.pair_empty : Set := {empty.toObject, singleton_empty.toObject}

Exercise 3.1.2

theorem declaration uses 'sorry'SetTheory.Set.emptyset_neq_singleton : empty ≠ singleton_empty := byinst✝:SetTheory⊢ empty ≠ singleton_empty sorryAll goals completed! 🐙

Exercise 3.1.2

theorem declaration uses 'sorry'SetTheory.Set.emptyset_neq_pair : empty ≠ pair_empty := byinst✝:SetTheory⊢ empty ≠ pair_empty sorryAll goals completed! 🐙

Exercise 3.1.2

theorem declaration uses 'sorry'SetTheory.Set.singleton_empty_neq_pair : singleton_empty ≠ pair_empty := byinst✝:SetTheory⊢ singleton_empty ≠ pair_empty sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.union_congr_left (A A' B:Set) (h: A = A') : A ∪ B = A' ∪ B := byinst✝:SetTheoryA:SetA':SetB:Seth:A = A'⊢ A ∪ B = A' ∪ B sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.union_congr_right (A B B':Set) (h: B = B') : A ∪ B = A ∪ B' := byinst✝:SetTheoryA:SetB:SetB':Seth:B = B'⊢ A ∪ B = A ∪ B' sorryAll goals completed! 🐙

Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3

theorem declaration uses 'sorry'SetTheory.Set.singleton_union_singleton (a b:Object) : ({a}:Set) ∪ ({b}:Set) = {a,b} := byinst✝:SetTheorya:Objectb:Object⊢ {a} ∪ {b} = {a, b} sorryAll goals completed! 🐙

Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3

theorem declaration uses 'sorry'SetTheory.Set.union_comm (A B:Set) : A ∪ B = B ∪ A := byinst✝:SetTheoryA:SetB:Set⊢ A ∪ B = B ∪ A sorryAll goals completed! 🐙

Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3

theorem declaration uses 'sorry'SetTheory.Set.union_assoc (A B C:Set) : (A ∪ B) ∪ C = A ∪ (B ∪ C) := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ∪ C = A ∪ (B ∪ C) -- this proof is written to follow the structure of the original text. apply exthinst✝:SetTheoryA:SetB:SetC:Set⊢ ∀ (x : Object), x ∈ A ∪ B ∪ C ↔ x ∈ A ∪ (B ∪ C) intro xhinst✝:SetTheoryA:SetB:SetC:Setx:Object⊢ x ∈ A ∪ B ∪ C ↔ x ∈ A ∪ (B ∪ C) constructorh.mpinst✝:SetTheoryA:SetB:SetC:Setx:Object⊢ x ∈ A ∪ B ∪ C → x ∈ A ∪ (B ∪ C)h.mprinst✝:SetTheoryA:SetB:SetC:Setx:Object⊢ x ∈ A ∪ (B ∪ C) → x ∈ A ∪ B ∪ C .h.mpinst✝:SetTheoryA:SetB:SetC:Setx:Object⊢ x ∈ A ∪ B ∪ C → x ∈ A ∪ (B ∪ C) intro hxh.mpinst✝:SetTheoryA:SetB:SetC:Setx:Objecthx:x ∈ A ∪ B ∪ C⊢ x ∈ A ∪ (B ∪ C) rw [mem_union] at hxh.mpinst✝:SetTheoryA:SetB:SetC:Setx:Objecthx:x ∈ A ∪ B ∨ x ∈ C⊢ x ∈ A ∪ (B ∪ C) rcases hx with case1 | case2h.mp.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1:x ∈ A ∪ B⊢ x ∈ A ∪ (B ∪ C)h.mp.inrinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase2:x ∈ C⊢ x ∈ A ∪ (B ∪ C) .h.mp.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1:x ∈ A ∪ B⊢ x ∈ A ∪ (B ∪ C) rw [mem_union] at case1h.mp.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1:x ∈ A ∨ x ∈ B⊢ x ∈ A ∪ (B ∪ C) rcases case1 with case1a | case1bh.mp.inl.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1a:x ∈ A⊢ x ∈ A ∪ (B ∪ C)h.mp.inl.inrinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1b:x ∈ B⊢ x ∈ A ∪ (B ∪ C) .h.mp.inl.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1a:x ∈ A⊢ x ∈ A ∪ (B ∪ C) rw [mem_union]h.mp.inl.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1a:x ∈ A⊢ x ∈ A ∨ x ∈ B ∪ C; tautoAll goals completed! 🐙 have : x ∈ B ∪ C := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ∪ C = A ∪ (B ∪ C) rw [mem_union]inst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1b:x ∈ B⊢ x ∈ B ∨ x ∈ C; tautoAll goals completed! 🐙 rw [mem_union]h.mp.inl.inrinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1b:x ∈ Bthis:x ∈ B ∪ C⊢ x ∈ A ∨ x ∈ B ∪ C; tautoAll goals completed! 🐙 have : x ∈ B ∪ C := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ∪ C = A ∪ (B ∪ C) rw [mem_union]inst✝:SetTheoryA:SetB:SetC:Setx:Objectcase2:x ∈ C⊢ x ∈ B ∨ x ∈ C; tautoAll goals completed! 🐙 rw [mem_union]h.mp.inrinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase2:x ∈ Cthis:x ∈ B ∪ C⊢ x ∈ A ∨ x ∈ B ∪ C; tautoAll goals completed! 🐙 sorryAll goals completed! 🐙

Proposition 3.1.27(c)

theorem declaration uses 'sorry'SetTheory.Set.union_self (A:Set) : A ∪ A = A := byinst✝:SetTheoryA:Set⊢ A ∪ A = A sorryAll goals completed! 🐙

Proposition 3.1.27(a)

theorem declaration uses 'sorry'SetTheory.Set.union_empty (A:Set) : A ∪ ∅ = A := byinst✝:SetTheoryA:Set⊢ A ∪ ∅ = A sorryAll goals completed! 🐙

Proposition 3.1.27(a)

theorem declaration uses 'sorry'SetTheory.Set.empty_union (A:Set) : ∅ ∪ A = A := byinst✝:SetTheoryA:Set⊢ ∅ ∪ A = A sorryAll goals completed! 🐙theorem SetTheory.Set.triple_eq (a b c:Object) : {a,b,c} = ({a}:Set) ∪ {b,c} := byinst✝:SetTheorya:Objectb:Objectc:Object⊢ {a, b, c} = {a} ∪ {b, c} rflAll goals completed! 🐙

Example 3.1.10

theorem declaration uses 'sorry'SetTheory.Set.pair_union_pair (a b c:Object) : ({a,b}:Set) ∪ {b,c} = {a,b,c} := sorry

Definition 3.1.14.

instance SetTheory.Set.uinstSubset : HasSubset Set where Subset X Y := ∀ x, x ∈ X → x ∈ Y

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

instance SetTheory.Set.instSSubset : HasSSubset Set where SSubset X Y := X ⊆ Y ∧ X ≠ Y

Definition 3.1.14.

theorem SetTheory.Set.subset_def (X Y:Set) : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y := byinst✝:SetTheoryX:SetY:Set⊢ X ⊆ Y ↔ ∀ x ∈ X, x ∈ Y rflAll goals completed! 🐙

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

theorem SetTheory.Set.ssubset_def (X Y:Set) : X ⊂ Y ↔ (X ⊆ Y ∧ X ≠ Y) := byinst✝:SetTheoryX:SetY:Set⊢ X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y rflAll goals completed! 🐙

Remark 3.1.15

theorem declaration uses 'sorry'SetTheory.Set.subset_congr_left {A A' B:Set} (hAA':A = A') (hAB: A ⊆ B) : A' ⊆ B := byinst✝:SetTheoryA:SetA':SetB:SethAA':A = A'hAB:A ⊆ B⊢ A' ⊆ B sorryAll goals completed! 🐙

Examples 3.1.16

theorem declaration uses 'sorry'SetTheory.Set.subset_self (A:Set) : A ⊆ A := byinst✝:SetTheoryA:Set⊢ A ⊆ A sorryAll goals completed! 🐙

Examples 3.1.16

theorem declaration uses 'sorry'SetTheory.Set.empty_subset (A:Set) : ∅ ⊆ A := byinst✝:SetTheoryA:Set⊢ ∅ ⊆ A sorryAll goals completed! 🐙

Proposition 3.1.17 (Partial ordering by set inclusion)

theorem SetTheory.Set.subset_trans (A B C:Set) (hAB:A ⊆ B) (hBC:B ⊆ C) : A ⊆ C := byinst✝:SetTheoryA:SetB:SetC:SethAB:A ⊆ BhBC:B ⊆ C⊢ A ⊆ C -- this proof is written to follow the structure of the original text. rw [subset_def]inst✝:SetTheoryA:SetB:SetC:SethAB:A ⊆ BhBC:B ⊆ C⊢ ∀ x ∈ A, x ∈ C intro x hxinst✝:SetTheoryA:SetB:SetC:SethAB:A ⊆ BhBC:B ⊆ Cx:Objecthx:x ∈ A⊢ x ∈ C rw [subset_def] at hABinst✝:SetTheoryA:SetB:SetC:SethAB:∀ x ∈ A, x ∈ BhBC:B ⊆ Cx:Objecthx:x ∈ A⊢ x ∈ C replace hx := hAB x hxinst✝:SetTheoryA:SetB:SetC:SethAB:∀ x ∈ A, x ∈ BhBC:B ⊆ Cx:Objecthx:x ∈ B⊢ x ∈ C replace hx := hBC x hxinst✝:SetTheoryA:SetB:SetC:SethAB:∀ x ∈ A, x ∈ BhBC:B ⊆ Cx:Objecthx:x ∈ C⊢ x ∈ C assumptionAll goals completed! 🐙

Proposition 3.1.17 (Partial ordering by set inclusion)

theorem declaration uses 'sorry'SetTheory.Set.subset_antisymm (A B:Set) (hAB:A ⊆ B) (hBA:B ⊆ A) : A = B := byinst✝:SetTheoryA:SetB:SethAB:A ⊆ BhBA:B ⊆ A⊢ A = B sorryAll goals completed! 🐙

Proposition 3.1.17 (Partial ordering by set inclusion)

theorem declaration uses 'sorry'SetTheory.Set.ssubset_trans (A B C:Set) (hAB:A ⊂ B) (hBC:B ⊂ C) : A ⊂ C := byinst✝:SetTheoryA:SetB:SetC:SethAB:A ⊂ BhBC:B ⊂ C⊢ A ⊂ C sorryAll goals completed! 🐙

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

abbrev SetTheory.Set.toSubtype (A:Set) := Subtype (fun x ↦ x ∈ A)instance : CoeSort (Set) (Type) where coe A := A.toSubtype/-- 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). -/ lemma SetTheory.Set.subtype_property (A:Set) (x:A) : x.val ∈ A := x.propertylemma SetTheory.Set.subtype_coe (A:Set) (x:A) : x.val = x := rfllemma SetTheory.Set.coe_inj (A:Set) (x y:A) : x.val = y.val ↔ x = y := Subtype.coe_inj

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.

def SetTheory.Set.subtype_mk (A:Set) {x:Object} (hx:x ∈ A) : A := ⟨ x, hx ⟩lemma SetTheory.Set.subtype_mk_coe {A:Set} {x:Object} (hx:x ∈ A) : A.subtype_mk hx = x := byinst✝:SetTheoryA:Setx:Objecthx:x ∈ A⊢ ↑(A.subtype_mk hx) = x rflAll goals completed! 🐙abbrev SetTheory.Set.specify (A:Set) (P: A → Prop) : Set := SetTheory.specify A P

Axiom 3.6 (axiom of specification)

theorem SetTheory.Set.specification_axiom {A:Set} {P: A → Prop} {x:Object} (h: x ∈ A.specify P) : x ∈ A := (SetTheory.specification_axiom A P).1 x h

Axiom 3.6 (axiom of specification)

theorem SetTheory.Set.specification_axiom' {A:Set} (P: A → Prop) (x:A.toSubtype) : x.val ∈ A.specify P ↔ P x := (SetTheory.specification_axiom A P).2 xtheorem declaration uses 'sorry'SetTheory.Set.specify_subset {A:Set} (P: A → Prop) : A.specify P ⊆ A := byinst✝:SetTheoryA:SetP:A.toSubtype → Prop⊢ A.specify P ⊆ A sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.specify_congr {A A':Set} (hAA':A = A') {P: A → Prop} {P': A' → Prop} (hPP': (x:Object) → (h:x ∈ A) → (h':x ∈ A') → P ⟨ x, h⟩ ↔ P' ⟨ x, h'⟩ ) : A.specify P = A'.specify P' := byinst✝:SetTheoryA:SetA':SethAA':A = A'P:A.toSubtype → PropP':A'.toSubtype → ProphPP':∀ (x : Object) (h : x ∈ A) (h' : x ∈ A'), P ⟨x, h⟩ ↔ P' ⟨x, h'⟩⊢ A.specify P = A'.specify P' sorryAll goals completed! 🐙instance SetTheory.Set.instIntersection : Inter Set where inter X Y := X.specify (fun x ↦ x.val ∈ Y)

Definition 3.1.22 (Intersections)

theorem SetTheory.Set.mem_inter (x:Object) (X Y:Set) : x ∈ (X ∩ Y) ↔ (x ∈ X ∧ x ∈ Y) := byinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y constructormpinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∩ Y → x ∈ X ∧ x ∈ Ymprinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∧ x ∈ Y → x ∈ X ∩ Y .mpinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∩ Y → x ∈ X ∧ x ∈ Y intro hmpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X ∩ Y⊢ x ∈ X ∧ x ∈ Y have h' := specification_axiom hmpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X ∩ Yh':x ∈ X⊢ x ∈ X ∧ x ∈ Y simp [h']mpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X ∩ Yh':x ∈ X⊢ x ∈ Y exact (specification_axiom' _ ⟨ x, h' ⟩).mp hAll goals completed! 🐙 intro ⟨ hX, hY ⟩mprinst✝:SetTheoryx:ObjectX:SetY:SethX:x ∈ XhY:x ∈ Y⊢ x ∈ X ∩ Y exact (specification_axiom' (fun x ↦ x.val ∈ Y) ⟨ x,hX⟩).mpr hYAll goals completed! 🐙instance SetTheory.Set.instSDiff : SDiff Set where sdiff X Y := X.specify (fun x ↦ x.val ∉ Y)

Definition 3.1.26 (Difference sets)

theorem SetTheory.Set.mem_sdiff (x:Object) (X Y:Set) : x ∈ (X \ Y) ↔ (x ∈ X ∧ x ∉ Y) := byinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X \ Y ↔ x ∈ X ∧ x ∉ Y constructormpinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X \ Y → x ∈ X ∧ x ∉ Ymprinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∧ x ∉ Y → x ∈ X \ Y .mpinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X \ Y → x ∈ X ∧ x ∉ Y intro hmpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X \ Y⊢ x ∈ X ∧ x ∉ Y have h' := specification_axiom hmpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X \ Yh':x ∈ X⊢ x ∈ X ∧ x ∉ Y simp [h']mpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X \ Yh':x ∈ X⊢ x ∉ Y exact (specification_axiom' _ ⟨ x, h' ⟩ ).mp hAll goals completed! 🐙 intro ⟨ hX, hY ⟩mprinst✝:SetTheoryx:ObjectX:SetY:SethX:x ∈ XhY:x ∉ Y⊢ x ∈ X \ Y exact (specification_axiom' (fun x ↦ x.val ∉ Y) ⟨ x, hX⟩ ).mpr hYAll goals completed! 🐙

Proposition 3.1.27(d) / Exercise 3.1.6

theorem declaration uses 'sorry'SetTheory.Set.inter_comm (A B:Set) : A ∩ B = B ∩ A := byinst✝:SetTheoryA:SetB:Set⊢ A ∩ B = B ∩ A sorryAll goals completed! 🐙

Proposition 3.1.27(b)

theorem declaration uses 'sorry'SetTheory.Set.subset_union {A X: Set} (hAX: A ⊆ X) : A ∪ X = X := byinst✝:SetTheoryA:SetX:SethAX:A ⊆ X⊢ A ∪ X = X sorryAll goals completed! 🐙

Proposition 3.1.27(b)

theorem declaration uses 'sorry'SetTheory.Set.union_subset {A X: Set} (hAX: A ⊆ X) : X ∪ A = X := byinst✝:SetTheoryA:SetX:SethAX:A ⊆ X⊢ X ∪ A = X sorryAll goals completed! 🐙

Proposition 3.1.27(c)

theorem declaration uses 'sorry'SetTheory.Set.inter_self (A:Set) : A ∩ A = A := byinst✝:SetTheoryA:Set⊢ A ∩ A = A sorryAll goals completed! 🐙

Proposition 3.1.27(e)

theorem declaration uses 'sorry'SetTheory.Set.inter_assoc (A B C:Set) : (A ∩ B) ∩ C = A ∩ (B ∩ C) := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∩ B ∩ C = A ∩ (B ∩ C) sorryAll goals completed! 🐙

Proposition 3.1.27(f)

theorem declaration uses 'sorry'SetTheory.Set.inter_union_distrib_left (A B C:Set) : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := sorry

Proposition 3.1.27(f)

theorem declaration uses 'sorry'SetTheory.Set.union_inter_distrib_left (A B C:Set) : A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C) := sorry

Proposition 3.1.27(f)

theorem declaration uses 'sorry'SetTheory.Set.union_compl {A X:Set} (hAX: A ⊆ X) : A ∪ (X \ A) = X := byinst✝:SetTheoryA:SetX:SethAX:A ⊆ X⊢ A ∪ X \ A = X sorryAll goals completed! 🐙

Proposition 3.1.27(f)

theorem declaration uses 'sorry'SetTheory.Set.inter_compl {A X:Set} (hAX: A ⊆ X) : A ∩ (X \ A) = ∅ := byinst✝:SetTheoryA:SetX:SethAX:A ⊆ X⊢ A ∩ (X \ A) = ∅ sorryAll goals completed! 🐙

Proposition 3.1.27(g)

theorem declaration uses 'sorry'SetTheory.Set.compl_union {A B X:Set} (hAX: A ⊆ X) (hBX: B ⊆ X) : X \ (A ∪ B) = (X \ A) ∩ (X \ B) := byinst✝:SetTheoryA:SetB:SetX:SethAX:A ⊆ XhBX:B ⊆ X⊢ X \ (A ∪ B) = X \ A ∩ (X \ B) sorryAll goals completed! 🐙

Proposition 3.1.27(g)

theorem declaration uses 'sorry'SetTheory.Set.compl_inter {A B X:Set} (hAX: A ⊆ X) (hBX: B ⊆ X) : X \ (A ∩ B) = (X \ A) ∪ (X \ B) := byinst✝:SetTheoryA:SetB:SetX:SethAX:A ⊆ XhBX:B ⊆ X⊢ X \ (A ∩ B) = X \ A ∪ X \ B sorryAll goals completed! 🐙

Not from textbook: sets form a distributive lattice.

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.instDistribLattice : DistribLattice Set where le := (· ⊆ ·) le_refl := subset_self le_trans := subset_trans le_antisymm := subset_antisymm inf := (· ∩ ·) sup := (· ∪ ·) le_sup_left := byinst✝:SetTheory⊢ ∀ (a b : Set), a ⊆ a ∪ b sorryAll goals completed! 🐙 le_sup_right := byinst✝:SetTheory⊢ ∀ (a b : Set), b ⊆ a ∪ b sorryAll goals completed! 🐙 sup_le := byinst✝:SetTheory⊢ ∀ (a b c : Set), a ⊆ c → b ⊆ c → a ∪ b ⊆ c sorryAll goals completed! 🐙 inf_le_left := byinst✝:SetTheory⊢ ∀ (a b : Set), a ∩ b ⊆ a sorryAll goals completed! 🐙 inf_le_right := byinst✝:SetTheory⊢ ∀ (a b : Set), a ∩ b ⊆ b sorryAll goals completed! 🐙 le_inf := byinst✝:SetTheory⊢ ∀ (a b c : Set), a ⊆ b → a ⊆ c → a ⊆ b ∩ c sorryAll goals completed! 🐙 le_sup_inf := byinst✝:SetTheory⊢ ∀ (x y z : Set), (x ⊔ y) ⊓ (x ⊔ z) ⊆ x ⊔ y ⊓ z intro X Y Zinst✝:SetTheoryX:SetY:SetZ:Set⊢ (X ⊔ Y) ⊓ (X ⊔ Z) ⊆ X ⊔ Y ⊓ Z change (X ∪ Y) ∩ (X ∪ Z) ⊆ X ∪ (Y ∩ Z)inst✝:SetTheoryX:SetY:SetZ:Set⊢ (X ∪ Y) ∩ (X ∪ Z) ⊆ X ∪ Y ∩ Z rw [←union_inter_distrib_left]inst✝:SetTheoryX:SetY:SetZ:Set⊢ X ∪ Y ∩ Z ⊆ X ∪ Y ∩ Z exact subset_self _All goals completed! 🐙

Sets have a minimal element.

instance SetTheory.Set.instOrderBot : OrderBot Set where bot := ∅ bot_le := empty_subset

Definition of disjointness (using the previous instances)

theorem SetTheory.Set.disjoint_iff (A B:Set) : Disjoint A B ↔ A ∩ B = ∅ := byinst✝:SetTheoryA:SetB:Set⊢ Disjoint A B ↔ A ∩ B = ∅ convert _root_.disjoint_iffAll goals completed! 🐙abbrev SetTheory.Set.replace (A:Set) {P: A → Object → Prop} (hP : ∀ x y y', P x y ∧ P x y' → y = y') : Set := SetTheory.replace A P hP

Axiom 3.7 (Axiom of replacement)

theorem SetTheory.Set.replacement_axiom {A:Set} {P: A → Object → Prop} (hP: ∀ x y y', P x y ∧ P x y' → y = y') (y:Object) : y ∈ A.replace hP ↔ ∃ x, P x y := SetTheory.replacement_axiom A P hP yabbrev Nat := SetTheory.nat

Axiom 3.8 (Axiom of infinity)

def SetTheory.Set.nat_equiv : ℕ ≃ Nat := SetTheory.nat_equiv-- Below are some API for handling coercions. This may not be the optimal way to set things up. instance SetTheory.Set.instOfNat {n:ℕ} : OfNat Nat n where ofNat := nat_equiv ninstance SetTheory.Set.instNatCast : NatCast Nat where natCast n := nat_equiv ninstance SetTheory.Set.toNat : Coe Nat ℕ where coe n := nat_equiv.symm ninstance SetTheory.Object.instNatCast : NatCast Object where natCast n := (n:Nat).valinstance SetTheory.Object.instOfNat {n:ℕ} : OfNat Object n where ofNat := ((n:Nat):Object)@[simp] lemma SetTheory.Object.ofnat_eq {n:ℕ} : ((n:Nat):Object) = (n:Object) := rfllemma SetTheory.Object.ofnat_eq' {n:ℕ} : (ofNat(n):Object) = (n:Object) := rfllemma SetTheory.Set.nat_coe_eq {n:ℕ} : (n:Nat) = OfNat.ofNat n := rfl@[simp] lemma SetTheory.Set.nat_equiv_inj (n m:ℕ) : (n:Nat) = (m:Nat) ↔ n=m := Equiv.apply_eq_iff_eq nat_equiv@[simp] lemma SetTheory.Set.nat_equiv_symm_inj (n m:Nat) : (n:ℕ) = (m:ℕ) ↔ n = m := Equiv.apply_eq_iff_eq nat_equiv.symm@[simp] theorem SetTheory.Set.ofNat_inj (n m:ℕ) : (ofNat(n) : Nat) = (ofNat(m) : Nat) ↔ ofNat(n) = ofNat(m) := byinst✝:SetTheoryn:ℕm:ℕ⊢ OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m convert nat_equiv_inj _ _All goals completed! 🐙@[simp] theorem SetTheory.Set.ofNat_inj' (n m:ℕ) : (ofNat(n) : Object) = (ofNat(m) : Object) ↔ ofNat(n) = ofNat(m) := byinst✝:SetTheoryn:ℕm:ℕ⊢ OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m simp only [←Object.ofnat_eq, Object.ofnat_eq', Set.coe_inj, Set.nat_equiv_inj]inst✝:SetTheoryn:ℕm:ℕ⊢ n = m ↔ OfNat.ofNat n = OfNat.ofNat m rflAll goals completed! 🐙@[simp] lemma SetTheory.Set.nat_equiv_coe_of_coe (n:ℕ) : ((n:Nat):ℕ) = n := Equiv.symm_apply_apply nat_equiv n@[simp] lemma SetTheory.Set.nat_equiv_coe_of_coe' (n:Nat) : ((n:ℕ):Nat) = n := Equiv.symm_apply_apply nat_equiv.symm nexample : (5:Nat) ≠ (3:Nat) := byinst✝:SetTheory⊢ 5 ≠ 3 simpAll goals completed! 🐙example : (5:Object) ≠ (3:Object) := byinst✝:SetTheory⊢ 5 ≠ 3 simpAll goals completed! 🐙

Example 3.1.16 (simplified).

declaration uses 'sorry'example : ({3, 5}:Set) ⊆ {1, 3, 5} := byinst✝:SetTheory⊢ {3, 5} ⊆ {1, 3, 5} sorryAll goals completed! 🐙

Example 3.1.17 (simplified).

declaration uses 'sorry'example : ({3, 5}:Set).specify (fun x ↦ x.val ≠ 3) = {(5:Object)} := byinst✝:SetTheory⊢ ({3, 5}.specify fun x => ↑x ≠ 3) = {5} sorryAll goals completed! 🐙

Example 3.1.24

declaration uses 'sorry'example : ({1, 2, 4}:Set) ∩ {2,3,4} = {2, 4} := byinst✝:SetTheory⊢ {1, 2, 4} ∩ {2, 3, 4} = {2, 4} sorryAll goals completed! 🐙

Example 3.1.24

declaration uses 'sorry'example : ({1, 2}:Set) ∩ {3,4} = ∅ := byinst✝:SetTheory⊢ {1, 2} ∩ {3, 4} = ∅ sorryAll goals completed! 🐙declaration uses 'sorry'example : ¬ Disjoint ({1, 2, 3}:Set) {2,3,4} := byinst✝:SetTheory⊢ ¬Disjoint {1, 2, 3} {2, 3, 4} sorryAll goals completed! 🐙declaration uses 'sorry'example : Disjoint (∅:Set) ∅ := byinst✝:SetTheory⊢ Disjoint ∅ ∅ sorryAll goals completed! 🐙

Definition 3.1.26 example

declaration uses 'sorry'example : ({1, 2, 3, 4}:Set) \ {2,4,6} = {1, 3} := byinst✝:SetTheory⊢ {1, 2, 3, 4} \ {2, 4, 6} = {1, 3} sorryAll goals completed! 🐙

Example 3.1.30

declaration uses 'sorry'example : ({3,5,9}:Set).replace (P := fun x y ↦ ∃ (n:ℕ), x.val = n ∧ y = (n+1:ℕ)) (byinst✝:SetTheory⊢ ∀ (x : {3, 5, 9}.toSubtype) (y y' : Object), (fun x y => ∃ n, ↑x = ↑n ∧ y = ↑(n + 1)) x y ∧ (fun x y => ∃ n, ↑x = ↑n ∧ y = ↑(n + 1)) x y' → y = y' sorryAll goals completed! 🐙) = {4,6,10} := byinst✝:SetTheory⊢ {3, 5, 9}.replace ⋯ = {4, 6, 10} sorryAll goals completed! 🐙

Example 3.1.31

declaration uses 'sorry'example : ({3,5,9}:Set).replace (P := fun x y ↦ y=1) (byinst✝:SetTheory⊢ ∀ (x : {3, 5, 9}.toSubtype) (y y' : Object), (fun x y => y = 1) x y ∧ (fun x y => y = 1) x y' → y = y' sorryAll goals completed! 🐙) = {1} := byinst✝:SetTheory⊢ {3, 5, 9}.replace ⋯ = {1} sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.subset_tfae (A B C:Set) : [A ⊆ B, A ∪ B = B, A ∩ B = A].TFAE := byinst✝:SetTheoryA:SetB:SetC:Set⊢ [A ⊆ B, A ∪ B = B, A ∩ B = A].TFAE sorryAll goals completed! 🐙

Exercise 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.inter_subset_left (A B:Set) : A ∩ B ⊆ A := byinst✝:SetTheoryA:SetB:Set⊢ A ∩ B ⊆ A sorryAll goals completed! 🐙

Exercise 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.inter_subset_right (A B:Set) : A ∩ B ⊆ B := byinst✝:SetTheoryA:SetB:Set⊢ A ∩ B ⊆ B sorryAll goals completed! 🐙

Exercise 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.subset_inter_iff (A B C:Set) : C ⊆ A ∩ B ↔ C ⊆ A ∧ C ⊆ B := byinst✝:SetTheoryA:SetB:SetC:Set⊢ C ⊆ A ∩ B ↔ C ⊆ A ∧ C ⊆ B sorryAll goals completed! 🐙

Exercise 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.subset_union_left (A B:Set) : A ⊆ A ∪ B := byinst✝:SetTheoryA:SetB:Set⊢ A ⊆ A ∪ B sorryAll goals completed! 🐙

Exercise 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.subset_union_right (A B:Set) : B ⊆ A ∪ B := byinst✝:SetTheoryA:SetB:Set⊢ B ⊆ A ∪ B sorryAll goals completed! 🐙

Exercise 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.union_subset_iff (A B C:Set) : A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C sorryAll goals completed! 🐙

Exercise 3.1.8

theorem declaration uses 'sorry'SetTheory.Set.inter_union_cancel (A B:Set) : A ∩ (A ∪ B) = A := byinst✝:SetTheoryA:SetB:Set⊢ A ∩ (A ∪ B) = A sorryAll goals completed! 🐙

Exercise 3.1.8

theorem declaration uses 'sorry'SetTheory.Set.union_inter_cancel (A B:Set) : A ∪ (A ∩ B) = A := byinst✝:SetTheoryA:SetB:Set⊢ A ∪ A ∩ B = A sorryAll goals completed! 🐙

Exercise 3.1.9

theorem declaration uses 'sorry'SetTheory.Set.partition_left {A B X:Set} (h_union: A ∪ B = X) (h_inter: A ∩ B = ∅) : A = X \ B := byinst✝:SetTheoryA:SetB:SetX:Seth_union:A ∪ B = Xh_inter:A ∩ B = ∅⊢ A = X \ B sorryAll goals completed! 🐙

Exercise 3.1.9

theorem declaration uses 'sorry'SetTheory.Set.partition_right {A B X:Set} (h_union: A ∪ B = X) (h_inter: A ∩ B = ∅) : B = X \ A := byinst✝:SetTheoryA:SetB:SetX:Seth_union:A ∪ B = Xh_inter:A ∩ B = ∅⊢ B = X \ A sorryAll goals completed! 🐙

Exercise 3.1.10

theorem declaration uses 'sorry'Set.pairwise_disjoint (A B:Set) : Pairwise (Function.onFun Disjoint ![A \ B, A ∩ B, B \ A]) := byinst✝:SetTheoryA:SetB:Set⊢ Pairwise (Function.onFun Disjoint ![A \ B, A ∩ B, B \ A]) sorryAll goals completed! 🐙

Exercise 3.1.10

theorem declaration uses 'sorry'Set.union_eq_partition (A B:Set) : A ∪ B = (A \ B) ∪ (A ∩ B) ∪ (B \ A) := byinst✝:SetTheoryA:SetB:Set⊢ A ∪ B = A \ B ∪ A ∩ B ∪ B \ A sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.specification_from_replacement {A:Set} {P: A → Prop} : ∃ B, A ⊆ B ∧ ∀ x, x.val ∈ B ↔ P x := byinst✝:SetTheoryA:SetP:A.toSubtype → Prop⊢ ∃ B, A ⊆ B ∧ ∀ (x : A.toSubtype), ↑x ∈ B ↔ P x sorryAll goals completed! 🐙

Exercise 3.1.12.

theorem declaration uses 'sorry'SetTheory.Set.subset_union_subset {A B A' B':Set} (hA'A: A' ⊆ A) (hB'B: B' ⊆ B) : A ∪ A' ⊆ A ∪ B := byinst✝:SetTheoryA:SetB:SetA':SetB':SethA'A:A' ⊆ AhB'B:B' ⊆ B⊢ A ∪ A' ⊆ A ∪ B sorryAll goals completed! 🐙

Exercise 3.1.12.

theorem declaration uses 'sorry'SetTheory.Set.subset_inter_subset {A B A' B':Set} (hA'A: A' ⊆ A) (hB'B: B' ⊆ B) : A ∩ A' ⊆ A ∩ B := byinst✝:SetTheoryA:SetB:SetA':SetB':SethA'A:A' ⊆ AhB'B:B' ⊆ B⊢ A ∩ A' ⊆ A ∩ B sorryAll goals completed! 🐙

Exercise 3.1.12.

theorem declaration uses 'sorry'SetTheory.Set.subset_diff_subset_counter : ∃ (A B A' B':Set), (A' ⊆ A) ∧ (B' ⊆ B) ∧ ¬ (A \ A') ⊆ (B ∩ B') := byinst✝:SetTheory⊢ ∃ A B A' B', A' ⊆ A ∧ B' ⊆ B ∧ ¬A \ A' ⊆ B ∩ B' sorryAll goals completed! 🐙/- Final part of Exercise 3.1.12: state and prove a reasonable substitute positive result for the above theorem that involves set differences . -/

Exercise 3.1.13

theorem declaration uses 'sorry'SetTheory.Set.singleton_iff (A:Set) (hA: A ≠ ∅) : ¬ ∃ B, B ⊂ A ↔ ∃ x, A = {x} := byinst✝:SetTheoryA:SethA:A ≠ ∅⊢ ¬∃ B, B ⊂ A ↔ ∃ x, A = {x} sorryAll goals completed! 🐙end Chapter3