Sets

What we will learn here.

Let \(\mathbb{R}\) denote the real numbers. We’re going to talk about subsets of the reals here. We could use any type - we use the real numbers initially because they’re not so scary.

In Lean, X : set ℝ means that X is a set of real numbers (or equivalently, X is a subset of ℝ). If a is a real number, then a ∈ X means that a is an element of X. In this chapter, we will learn how to work with unions X ∪ Y, intersections X ∩ Y and inclusions X ⊆ Y of sets, and how to prove basic facts about these things in Lean. The key trick is that X : set ℝ is internally represented as a map ℝ → Prop.

Introduction

Let X be a set of real numbers. For any real number a we can ask if a is an element of X. The notation for this is a ∈ X, and of course it is a true/false statement, that is, a proposition. So given a set X we get a map ℝ → Prop, sending a real number a to the true/false statement a ∈ X. For example, if X is just the set {6} containng one element 6, then the associated map ℝ → Prop sends a real number a to the true/false statement a = 6. To give another example – if X is the set of positive real numbers, the associated map ℝ → Prop sends a to the true/false statement a > 0.

Conversely, if p : ℝ → Prop is a function sending real numbers to true/false statements, then p divides the real numbers into two parts, namely the real numbers a such that p a is true, and those such that p a is false. So we could define a set X associated to p, by letting X be exactly the real numbers for which p a is true. For example if p : ℝ → Prop is the function sending a real number a to the statement a ^ 2 = 4, the corresponding subset X of real numbers is the real numbers a whose square equals 4, so X = {2, -2}.

Hence what we have here is two different ways of thinking about the same concept. Given a subset of the real numbers, we get a map ℝ → Prop, and conversely given such a map we can recover the subset as the real numbers being sent to the propositions which are true.

Inclusions

Let X and Y be subsets of the real numbers, with corresponding functions pX and pY : ℝ → Prop. We say that X is a subset of Y, and write X ⊆ Y, if every element of X is also an element of Y. We could write this as “for all real numbers a, a ∈ X → a ∈ Y. So in fact the subset symbol ⊆ is just a disguised version of an implication of the form P → Q, and we have seen how to prove such things in Lean. Let’s prove that every set X of reals is a subset of itself by just treating ⊆ as what it really means.

try it!

import data.real.basic

example (X : set ℝ) : X ⊆ X :=
begin
  -- remember the goal is just an elaborate notation
  -- for the proposition ∀ x : ℝ, x ∈ X → x ∈ X
  intro x,
  intro Hx,
  exact Hx,
end

[It’s probably worth mentioning that such fundamental facts like this are already in Lean and can be hence proved directly in one line. The result is known as “reflexivity of the subset relation” and a shorter proof looks like this:

try it!

import data.real.basic

example (X : set ℝ) : X ⊆ X := set.subset.refl X

]

Let’s do a more complicated example. Let’s start with two real numbers s and t, with s<t. If r is another real number, with r<s, then of course r<t. How do we know this? As mathematicians we are well aware that the statements r<s and s<t imply that r<t. This basic fact has a name – “transitivity of the < relation”. Lean just calls it lt_trans.

try it!

import data.real.basic

example (r s t : ℝ) (Hrs : r < s) (Hst : s < t) : r < t :=
begin
  exact lt_trans Hrs Hst
end

Let’s stay with our fixed real numbers s and t with s < t, and let’s introduce some sets. We let \(X=\{x\in\mathbb{R}\,\mid\,x<s\}\) and \(Y=\{x\in\mathbb{R}\,\mid\,x<t\}\).

DRAW A PICTURE

We see \(X\subseteq Y\) from the picture. Let’s prove it in Lean.

try it!

import data.real.basic

example (s t : ℝ) (Hst : s < t) : {x : ℝ | x < s} ⊆ {x : ℝ | x < t} :=
begin
  intro a,
  intro Ha,
  change a < s at Ha,
  show a < t,
  exact lt_trans Ha Hst,
end

The change and show commands do the same thing and I don’t really know why they have different names; change works on a hypothesis and show on the goal. Both of them can be used to simplify a proposition to something which is by definition the same. For example the proposition a ∈ {x : ℝ | x < s} literally means by definition that x < s is true when you let x = a, so it literally means a < s.

Intersections ∩ of sets

The intersection of two subsets X and Y of the real numbers is simply the real numbers which are in both X and Y. The notation is X ∩ Y and you get the intersection symbol in Lean by typing \cap.

Remember that a subset of the real numbers is just the same as a map R->prop. Let’s translate the idea of intersection into this language. The statement a ∈ X ∩ Y means exactly that a is in both X and Y. Let’s set Z = X ∩ Y. If pX is the map ℝ → Prop corresponding to X, and pY and pZ are defined similarly, then we see that pZ x, a.k.a. x ∈ Z, is equivalent to x ∈ X ∧ x ∈ Y, or in other words to pZ x ∧ pZ y.

We have already learnt techniques for proving goals like P ∧ Q → P and we can use these techniques to prove basic facts about sets such as A ∩ B \subseteq A.

try it!

import data.real.basic

example (X : set ℝ) (Y : set ℝ) : X ∩ Y ⊆ X :=
begin
  -- recall that ⊆ is really a → in disguise, so we can use intro.
  intro a,
  intro Ha,
  -- Ha is really an "and" statement in disguise, so we can use cases.
  cases Ha with Hx Hy,
  exact Hx
end

Exercise (symmetry of intersection)

Two sets are equal if and only if they have the same elements. Computer scientists call this “set extensionality” and in Lean the tactic for it is called ext. Run the code below in Lean, see what the line ext a does to the goal, and then use the usual suspects like split and cases to solve the goal.

try it!

import data.real.basic

example (X : set ℝ) (Y : set ℝ) : X ∩ Y = Y ∩ X :=
begin
  ext a
  sorry
end

Exercise (this has nothing to do with the real numbers)

Prove the same thing but for subsets of a general “Type”. I would encourage the use of cut and paste.

try it!

example (Ω : Type) (X : set Ω) (Y : set Ω) : X ∩ Y = Y ∩ X := sorry

Unions of sets.

If X and Y are subsets of the real numbers (or of any type), their union X ∪ Y is defined to be the elements of the type which are in either X or Y or both. You get the notation ∪ in Lean by typing cup. Just like ∩ is a disguised ∧, we have that ∪ is a disguised ∨. Let’s prove symmetry of ∪ using the things we know about propositions.

try it!

example (Ω : Type) (X : set Ω) (Y : set Ω) : X ∪ Y = Y ∪ X :=
begin
  ext a,
  split,
  { intro Ha,
    cases Ha,
      -- a in X
      right,assumption,
      -- a in Y
      left,assumption
  },
  { intro Ha,
    cases Ha,
      -- a in Y
      right,assumption,
      -- a in X
      left,assumption
  },
end

Exercise (set.subset_union_left)

try it!

example (Ω : Type) (X : set Ω) (Y : set Ω) : X ⊆ X ∪ Y :=
begin
  sorry
end

Exercise (logic and union)

try it!

example (Ω : Type) (A B C : set Ω) (x : Ω) (HC : x ∈ C)
  (HA : x ∉ A) (HB : x ∉ B) : ¬ (C ⊆ A ∪ B) :=
begin
  sorry
end