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

@[implicit_reducible]

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 }

@[implicit_reducible]

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

Axiom 3.1 (Sets are objects, coercion).

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

@[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, iff lemma).

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

@[implicit_reducible]

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 (∅ : Set) 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 ≠ ∅

@[implicit_reducible]

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.

@[implicit_reducible]

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

@[implicit_reducible]

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 (empty set is not a singleton)

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

Exercise 3.1.2 (empty set is not a pair)

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

Exercise 3.1.2 (singleton is not a pair)

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, singletons) / 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, commutativity) / 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, associativity) / Exercise 3.1.3

@[simp]

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

Proposition 3.1.27(c) (Union idempotent).

@[simp]

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

Proposition 3.1.27(a) (Union with empty).

@[simp]

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

Proposition 3.1.27(a) (Empty with union).

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

@[implicit_reducible]

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

Definition 3.1.14 (Subset).

Equations

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

@[implicit_reducible]

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

Definition 3.1.14 (Strict subset). 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

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

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

@[simp]

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

Examples 3.1.16 (the empty set is a subset)

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

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

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, strict transitivity)

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

@[implicit_reducible]

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

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, the property holds)

@[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, the specified set is a subset)

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.

@[implicit_reducible]

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)

@[implicit_reducible]

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) (Subset absorption).

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

Proposition 3.1.27(b) (Union absorption).

@[simp]

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

Proposition 3.1.27(c) (Intersection idempotent).

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) (Intersection distributes over union).

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) (Union distributes over intersection).

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

Proposition 3.1.27(f) (Partition of a superset).

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

Proposition 3.1.27(f) (Disjoint intersection with complement).

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

Proposition 3.1.27(g) (Complement of a union).

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

Proposition 3.1.27(g) (Complement of an intersection).

@[implicit_reducible]

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.

@[implicit_reducible]

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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 }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

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

Exercise 3.1.7 (b)

@[simp]

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

Exercise 3.1.7 (c)

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

Exercise 3.1.7 (d)

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

Exercise 3.1.7 (e)

@[simp]

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

Exercise 3.1.7 (f)

@[simp]

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

Exercise 3.1.8 (a)

@[simp]

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

Exercise 3.1.8 (b)

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

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

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

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

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 (differences: a counterexample)

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

Exercise 3.1.13

@[implicit_reducible]

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_1 : Object | x_1 ∈ {x}} = {x}

Compatibility of singleton

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

Compatibility of union

theorem Chapter3.SetTheory.Set.coe_pair [SetTheory] (x y : Object) : {x_1 : Object | x_1 ∈ {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 ∩ 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 \ 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