/-- A set of elements of `α` is a yes/no property of elements of `α`:
`A x` is the statement "`x` belongs to `A`". -/
def Set (α : Type u) : Type u := α → Prop/-- `x ∈ A` means that `x` has the property `A`. -/
instance instMembership : Membership α (Set α) := ⟨fun A x => A x⟩/-- `setOf p` is the set of all `x` with property `p`. We write it `{x | p x}` (notation below). -/
def setOf (p : α → Prop) : Set α := p/-- Belonging to `{x | p x}` means having property `p` — true by definition. -/
theorem mem_setOf (p : α → Prop) (a : α) : a ∈ {x | p x} ↔ p a := Iff.rfl/-- `A ⊆ B` ("`A` is a subset of `B`"): every member of `A` is a member of `B`.
(Mathlib states this with a strict-implicit `∀ ⦃x⦄`; we keep `x` explicit for readability.) -/
def Subset (A B : Set α) : Prop := ∀ x, x ∈ A → x ∈ B/-- Lets us write `A ⊆ B` for `Subset A B`. -/
instance instHasSubset : HasSubset (Set α) := ⟨Subset⟩/-- The union `A ∪ B`: everything in `A` *or* in `B` (or both). -/
def union (A B : Set α) : Set α := {x | x ∈ A ∨ x ∈ B}/-- Lets us write `A ∪ B`. -/
instance instUnion : Union (Set α) := ⟨union⟩/-- The intersection `A ∩ B`: everything in `A` *and* in `B`. -/
def inter (A B : Set α) : Set α := {x | x ∈ A ∧ x ∈ B}/-- Lets us write `A ∩ B`. -/
instance instInter : Inter (Set α) := ⟨inter⟩/-- The complement `Aᶜ`: everything (of type `α`) that is *not* in `A`. -/
def compl (A : Set α) : Set α := {x | x ∉ A}/-- The empty set: nothing belongs to it. (The underscore in `_x` says the name is unused.) -/
def empty : Set α := {_x | False}/-- Lets us write `∅` for the empty set. -/
instance instEmptyCollection : EmptyCollection (Set α) := ⟨empty⟩/-- The universal set: everything of type `α` belongs to it. -/
def univ : Set α := {_x | True}/-- The Cartesian product `A ×ˢ B`: all pairs `(a, b)` with `a ∈ A` and `b ∈ B`. -/
def prod (A : Set α) (B : Set β) : Set (α × β) := {p | p.1 ∈ A ∧ p.2 ∈ B}/-- `x ∈ A ∪ B` means `x ∈ A ∨ x ∈ B`. -/
theorem mem_union (x : α) (A B : Set α) : x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B := Iff.rfl/-- `x ∈ A ∩ B` means `x ∈ A ∧ x ∈ B`. -/
theorem mem_inter (x : α) (A B : Set α) : x ∈ A ∩ B ↔ x ∈ A ∧ x ∈ B := Iff.rfl/-- `x ∈ Aᶜ` means `x ∉ A`. -/
theorem mem_compl (x : α) (A : Set α) : x ∈ Aᶜ ↔ x ∉ A := Iff.rfl/-- **Extensionality.** Two sets are equal when they have exactly the same members.
This is where sets differ from lists: order and repetition are invisible.
The proof uses function extensionality and propositional extensionality, so the axiom
report lists `propext` and `Quot.sound` (from which `funext` is derived). -/
theorem ext {A B : Set α} (h : ∀ x, x ∈ A ↔ x ∈ B) : A = B :=
funext fun x => propext (h x)/-- Every set is a subset of itself. -/
theorem subset_refl (A : Set α) : A ⊆ A := by
intro x hx
exact hx/-- Inclusion is transitive: if `A ⊆ B` and `B ⊆ C` then `A ⊆ C`. -/
theorem subset_trans {A B C : Set α} (hAB : A ⊆ B) (hBC : B ⊆ C) : A ⊆ C := by
intro x hxA
have hxB : x ∈ B := hAB x hxA
exact hBC x hxB/-- The empty set is a subset of every set: there is no member of `∅` that could fail to be
in `A`. (Logicians say the statement is *vacuously* true.) -/
theorem empty_subset (A : Set α) : ∅ ⊆ A := by
intro x hx
-- `hx : x ∈ ∅` is a proof of `False`, and from `False` anything follows.
exact False.elim hx/-- Every set is a subset of the universal set. -/
theorem subset_univ (A : Set α) : A ⊆ univ := by
intro x _
-- `x ∈ univ` is just `True`.
trivial/-- `A ∩ B ⊆ A`: whatever is in both sets is, in particular, in the first one. -/
theorem inter_subset_left (A B : Set α) : A ∩ B ⊆ A := by
intro x hx
-- `hx : x ∈ A ∧ x ∈ B`; keep the left half.
exact hx.1/-- `A ∩ B ⊆ B`: whatever is in both sets is, in particular, in the second one. -/
theorem inter_subset_right (A B : Set α) : A ∩ B ⊆ B := by
intro x hx
-- `hx : x ∈ A ∧ x ∈ B`; keep the right half.
exact hx.2/-- `A ⊆ A ∪ B`: anything in `A` is in `A` or in `B`. -/
theorem subset_union_left (A B : Set α) : A ⊆ A ∪ B := by
intro x hx
exact Or.inl hx/-- Union is commutative: `A ∪ B = B ∪ A`. -/
theorem union_comm (A B : Set α) : A ∪ B = B ∪ A := by
apply ext
intro x
constructor
· intro h
-- `h : x ∈ A ∨ x ∈ B`, and "or" can be swapped.
exact Or.symm h
· intro h
exact Or.symm h/-- Intersection is commutative: `A ∩ B = B ∩ A`. -/
theorem inter_comm (A B : Set α) : A ∩ B = B ∩ A := by
apply ext
intro x
constructor
· intro h
-- `h : x ∈ A ∧ x ∈ B`, and "and" can be swapped.
exact And.symm h
· intro h
exact And.symm h/-- Intersection distributes over union: `A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)`.
(Mathlib analogue: `Set.inter_union_distrib_left`.) -/
theorem inter_union_distrib (A B C : Set α) : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := by
apply ext
intro x
constructor
· -- If `x ∈ A` and `x` is in `B` or `C`, look at which one.
intro ⟨hA, hBC⟩
cases hBC with
| inl hB => exact Or.inl ⟨hA, hB⟩
| inr hC => exact Or.inr ⟨hA, hC⟩
· -- Either way round, `x ∈ A`, and `x` is in `B` or in `C`.
intro h
cases h with
| inl hAB => exact ⟨hAB.1, Or.inl hAB.2⟩
| inr hAC => exact ⟨hAC.1, Or.inr hAC.2⟩/-- **De Morgan's law** for unions: `(A ∪ B)ᶜ = Aᶜ ∩ Bᶜ`.
Not being in `A ∪ B` means being in neither set. This proof is constructive: it does not
use the law of excluded middle. -/
theorem compl_union (A B : Set α) : (A ∪ B)ᶜ = Aᶜ ∩ Bᶜ := by
apply ext
intro x
constructor
· intro h
-- `h : ¬ (x ∈ A ∨ x ∈ B)`. If `x` were in `A`, it would be in `A ∪ B`; same for `B`.
exact ⟨fun hA => h (Or.inl hA), fun hB => h (Or.inr hB)⟩
· intro ⟨hnA, hnB⟩ hAB
-- `x` is in `A` or in `B`, and both cases contradict what we know.
cases hAB with
| inl hA => exact hnA hA
| inr hB => exact hnB hB/-- **De Morgan's law** for intersections: `(A ∩ B)ᶜ = Aᶜ ∪ Bᶜ`.
The direction `(A ∩ B)ᶜ ⊆ Aᶜ ∪ Bᶜ` needs **classical logic**: knowing only that `x` is not in
both sets, we must still decide *which* set it misses. We use excluded middle
(`Classical.em`), so the axiom report for this theorem includes `Classical.choice`. -/
theorem compl_inter (A B : Set α) : (A ∩ B)ᶜ = Aᶜ ∪ Bᶜ := by
apply ext
intro x
constructor
· intro h
-- `h : ¬ (x ∈ A ∧ x ∈ B)`. Either `x ∈ A` or not (excluded middle).
cases Classical.em (x ∈ A) with
| inl hA =>
-- Then `x` cannot also be in `B`.
exact Or.inr (fun hB => h ⟨hA, hB⟩)
| inr hnA => exact Or.inl hnA
· intro h ⟨hA, hB⟩
cases h with
| inl hnA => exact hnA hA
| inr hnB => exact hnB hB/-- A pair `(a, b)` is in `A ×ˢ B` exactly when `a ∈ A` and `b ∈ B`. True by definition. -/
theorem mem_prod (a : α) (b : β) (A : Set α) (B : Set β) :
(a, b) ∈ A ×ˢ B ↔ a ∈ A ∧ b ∈ B :=
Iff.rflEach exercise contains a sorry for you to replace. Open it in the Lean web editor, or clone the repository and run lake build.
/-- Show that `A ∩ B ⊆ B`.
Hint: start with `intro x hx`. What does `hx : x ∈ A ∩ B` tell you? -/
theorem inter_subset_right (A B : Set α) : A ∩ B ⊆ B := by
sorry/-- `A ∩ B ⊆ B`: whatever is in both sets is, in particular, in the second one. -/
theorem inter_subset_right (A B : Set α) : A ∩ B ⊆ B := by
intro x hx
-- `hx : x ∈ A ∧ x ∈ B`; keep the right half.
exact hx.2/-- Show that union is commutative.
Hint: `apply ext`, then `intro x` and `constructor`; `Or.symm` swaps the two sides of an "or". -/
theorem union_comm (A B : Set α) : A ∪ B = B ∪ A := by
sorry/-- Union is commutative: `A ∪ B = B ∪ A`. -/
theorem union_comm (A B : Set α) : A ∪ B = B ∪ A := by
apply ext
intro x
constructor
· intro h
-- `h : x ∈ A ∨ x ∈ B`, and "or" can be swapped.
exact Or.symm h
· intro h
exact Or.symm h/-- De Morgan's law: not being in `A ∪ B` means being in neither `A` nor `B`.
Hint: `x ∈ Aᶜ` means `x ∈ A → False`. You do not need classical logic for this one. -/
theorem compl_union (A B : Set α) : (A ∪ B)ᶜ = Aᶜ ∩ Bᶜ := by
sorry/-- **De Morgan's law** for unions: `(A ∪ B)ᶜ = Aᶜ ∩ Bᶜ`.
Not being in `A ∪ B` means being in neither set. This proof is constructive: it does not
use the law of excluded middle. -/
theorem compl_union (A B : Set α) : (A ∪ B)ᶜ = Aᶜ ∩ Bᶜ := by
apply ext
intro x
constructor
· intro h
-- `h : ¬ (x ∈ A ∨ x ∈ B)`. If `x` were in `A`, it would be in `A ∪ B`; same for `B`.
exact ⟨fun hA => h (Or.inl hA), fun hB => h (Or.inr hB)⟩
· intro ⟨hnA, hnB⟩ hAB
-- `x` is in `A` or in `B`, and both cases contradict what we know.
cases hAB with
| inl hA => exact hnA hA
| inr hB => exact hnB hB