Formalising Mathematics with Lean

4.3.Β Construction of the sequence of open setsπŸ”—

First we will construct a sequence of open sets over \mathbb{Q}\cap[0, 1], and then we will extend it to the rest of the rationals. Let Q = \mathbb{Q}\cap[0, 1]. To construct the sequence \{U_p ~|~ p \in Q\}, or, equivalently, the function G : Q \to \mathcal{P}(X), G(p) = U_p, we are going to proceed in the following way.

Since Q is countable, we consider the numbering Q = \{p_k ~|~ k \in \mathbb{N}\}, and we assume for simplicity that p_0 = 1 and that p_1 = 0. We are going to construct the open sets with condition (β˜…) by complete induction on k.

We take then, as the base of the induction,

  • U_1 = U_{p_0} = X.

  • U_0 = U_{p_1} the open set obtained when applying the characterisation of normal spaces (3.14) to the closed set C_1 and the open set C_2^c.

Trivially we have that \overline{U_0} \subseteq U_1 = X (with 0<1), hence (β˜…) is satisfied.

Now, for the inductive case, suppose we have defined U_{p_k} for each k = 0, 1, ..., n satisfying (β˜…), and now we want to construct U_{p_{n+1}}.

Note that the set \{p_0, p_1, ..., p_n\} \subset Q is not necessarily ordered. However, it is a finite set of rational numbers; therefore, we can find elements p_r and p_s such that p_r is the immediate predecessor of p_{n+1} and p_s is the immediate successor of p_{n+1}. That is, we have

p_r < p_{n+1} < p_s

and there is no k\leq n such that p_r < p_k < p_{n+1} nor p_{n+1} < p_k < p_s.

Since p_r < p_s, by the complete induction hypothesis we have that both are open and that \overline{U_{p_r}} \subseteq U_{p_s} (β˜…). We apply the characterisation of normal spaces (3.14) again, to find a new open set U = U_{p_{n+1}} such that

\overline{U_{p_r}} \subseteq U \subseteq \overline{U} \subseteq U_{p_s}

Which concludes the induction.

Let us now see how this is translated into Lean.

4.3.1.Β Numbering the rationalsπŸ”—

The rationals are countable, that is, there exists a bijection between \mathbb{N} and \mathbb{Q}. In particular, we need a function f : \mathbb{N} \to Q where Q = \mathbb{Q} \cap [0, 1], such that f is bijective, f(0) = 1 and f(1) = 0. That is, the function that takes each k \in \mathbb{N} to p_k.

lemma hf : βˆƒ f : β„• β†’ Q, (f.Bijective ∧ f 0 = ⟨1, Q1⟩ ∧ f 1 = ⟨0, Q0⟩) := ⊒ βˆƒ f, Function.Bijective f ∧ f 0 = ⟨1, Q1⟩ ∧ f 1 = ⟨0, Q0⟩

To prove the existence of such a function we need a series of previous results.

First of all, the countability of the rationals is already proved in Mathlib as Rat.instDenumerable. In order to extract a bijective function from this result, I have written the following lemma:

lemma bijective_nat_rat : βˆƒ f : β„• β†’ β„š, f.Bijective := ⊒ βˆƒ f, Function.Bijective f f:β„• ≃ β„šβŠ’ βˆƒ f, Function.Bijective f f:β„• ≃ β„šβŠ’ Function.Bijective ⇑f All goals completed! πŸ™

Evidently, by the proof irrelevance of Lean, we will not be able to evaluate this function explicitly. But we have the information we need from it.

Now, I want to prove that there exists a bijective function from \mathbb{N} to Q. Since we already have a bijective function from \mathbb{N} to \mathbb{Q}, the idea is to compose it with a bijection from \mathbb{Q} to Q.

To prove that this bijection exists, it suffices to prove that \mathbb{Q} and Q have the same cardinality (Cardinal.eq). But, in fact, any non-finite subset of \mathbb{Q} has cardinality \aleph_0 (proved in non_finite_rat_set_cardinal_aleph0). It suffices to prove that Q is not finite (proved in Q_not_finite).

lemma non_finite_rat_set_cardinal_aleph0 (A : Set β„š) (hA : Β¬ A.Finite) : Cardinal.mk ↑A = Cardinal.aleph0 := A:Set β„šhA:Β¬A.Finite⊒ Cardinal.mk ↑A = Cardinal.aleph0

Finally, any permutation of two values of a function preserves bijectivity (proved in permute_f_bijectivity). Therefore, we can force f(0) = 1 and f(1) = 0.

def permute_f {X Y : Type} [DecidableEq X] (f : X β†’ Y) (a b : X) : X β†’ Y := fun x ↦ if x = a then f b else if x = b then f a else f xlemma permute_f_bijectivity {X Y : Type} [DecidableEq X] {f : X β†’ Y} (a b : X) (h : f.Bijective) : (permute_f f a b).Bijective := X:TypeY:Typeinst✝:DecidableEq Xf:X β†’ Ya:Xb:Xh:Function.Bijective f⊒ Function.Bijective (permute_f f a b)

Once hf is proved, we can define f via Classical.choose and start working with it, even if we do not know it explicitly.

noncomputable def f : β„• β†’ Q := Classical.choose hf

For example, we can prove that it has an inverse.

lemma f_has_inverse : βˆƒ g, Function.LeftInverse g f ∧ Function.RightInverse g f := ⊒ βˆƒ g, Function.LeftInverse g f ∧ Function.RightInverse g f ⊒ Function.Bijective f All goals completed! πŸ™

4.3.2.Β Finding the immediate successor and predecessorπŸ”—

We now have each p_k defined in Lean as f(k) for each k \in \mathbb{N}. In order to define each open set U_{p_k}, we need to be able to find, for each set \{p_0, p_1, \dots, p_{n-1}\}, the immediate predecessor p_r and the immediate successor p_s of p_{n}.

Again, in Lean this is encoded as functions; we want to find a function r : \mathbb{N} \to \mathbb{N} that, for each n>1, returns the immediate predecessor of f(n), among \{f(k) ~|~ k < n\}, and likewise a function s : \mathbb{N} \to \mathbb{N} that finds the immediate successor. However, the existence of such functions is not trivial.

Lemma 4.1πŸ”—

Let n > 1. Then there exists an r_n < n such that f(r_n) < f(n), and if k < n is such that f(k) < f(n) then f(k) \leq f(r_n).

lemma exists_r (n : β„•) (hn : n > 1) : βˆƒ r ∈ Finset.range n, ((f r < f n) ∧ (βˆ€ m ∈ Finset.range n, f m < f n β†’ f m ≀ f r)) := n:β„•hn:n > 1⊒ βˆƒ r ∈ Finset.range n, f r < f n ∧ βˆ€ m ∈ Finset.range n, f m < f n β†’ f m ≀ f r

Proof. Let n>1. Consider the set

R = \{m : \mathbb{N} ~|~ m < n \land f(m) < f(n)\}

n:β„•hn:n > 1R:Finset β„• := {m ∈ Finset.range n | f m < f n}⊒ βˆƒ r ∈ Finset.range n, f r < f n ∧ βˆ€ m ∈ Finset.range n, f m < f n β†’ f m ≀ f r

R is a non-empty finite set, since 1 \in R

n:β„•hn:n > 1R:Finset β„• := {m ∈ Finset.range n | f m < f n}⊒ R.Nonemptyn:β„•hn:n > 1R:Finset β„• := {m ∈ Finset.range n | f m < f n}hR:R.Nonempty⊒ True n:β„•hn:n > 1R:Finset β„• := {m ∈ Finset.range n | f m < f n}⊒ R.Nonempty n:β„•hn:n > 1R:Finset β„• := {m ∈ Finset.range n | f m < f n}⊒ 1 ∈ R; All goals completed! πŸ™

We take the set f(R), which is also a finite and non-empty set, since R is, hence it has a maximum. We take the argument of the maximum of f(R), r_n = \arg \max \{f(m) ~|~ m \in R\}, and let us see that it satisfies the conditions we require.

n:β„•hn:n > 1R:Finset β„• := {m ∈ Finset.range n | f m < f n}hR:R.NonemptyfR:Finset ↑Q := Finset.image f R⊒ βˆƒ r ∈ Finset.range n, f r < f n ∧ βˆ€ m ∈ Finset.range n, f m < f n β†’ f m ≀ f r -- tomamos el conjunto de as imΓ‘genes de R -- vemos que no es vacΓ­o n:β„•hn:n > 1R:Finset β„• := {m ∈ Finset.range n | f m < f n}hR:R.NonemptyfR:Finset ↑Q := Finset.image f RhfR:fR.Nonempty⊒ βˆƒ r ∈ Finset.range n, f r < f n ∧ βˆ€ m ∈ Finset.range n, f m < f n β†’ f m ≀ f r -- tomamos el mΓ‘ximo de las imΓ‘genes n:β„•hn:n > 1R:Finset β„• := {m ∈ Finset.range n | f m < f n}hR:R.NonemptyfR:Finset ↑Q := Finset.image f RhfR:fR.Nonemptyfr:↑Q := fR.max' β‹―βŠ’ βˆƒ r ∈ Finset.range n, f r < f n ∧ βˆ€ m ∈ Finset.range n, f m < f n β†’ f m ≀ f r -- tomamos el argumento de fr, fr = f r obtain ⟨r, hr⟩ := Finset.mem_image.mp (n:β„•hn:n > 1R:Finset β„• := {m ∈ Finset.range n | f m < f n}hR:R.NonemptyfR:Finset ↑Q := Finset.image f RhfR:fR.Nonemptyfr:↑Q := fR.max' β‹―βŠ’ ?m.111 ∈ Finset.image ?m.109 ?m.110 All goals completed! πŸ™) n:β„•hn:n > 1R:Finset β„• := {m ∈ Finset.range n | f m < f n}hR:R.NonemptyfR:Finset ↑Q := Finset.image f RhfR:fR.Nonemptyfr:↑Q := fR.max' β‹―r:β„•hr:r ∈ R ∧ f r = fR.max' hfR⊒ r ∈ Finset.range n ∧ f r < f n ∧ βˆ€ m ∈ Finset.range n, f m < f n β†’ f m ≀ f r -- probamos que este r nos vale

We have that r \in R, hence r < n and f(r) < f(n). Let then k < n with f(k) < f(n). By construction, k \in R and therefore f(k) \in f(R). Since r is the argument of the maximum of f(R), f(r) is the maximum of f(R) and therefore f(k) \leq f(R), as we wanted. ∎

The complete proof is in the repository, as well as the analogue for s.

Having guaranteed the existence of these functions, we can now take the functions r and s and start working with them.

noncomputable def r : β„• β†’ β„• := fun n ↦ if h : n > 1 then Classical.choose (exists_r n h) else 1noncomputable def s : β„• β†’ β„• := fun n ↦ if h : n > 1 then Classical.choose (exists_s n h) else 0

Let us see the main properties of these two functions. First, we have the basic properties of r and s, which hold simply by construction.

Lemma 4.2πŸ”—

For each n > 1, we have:

\left\{ \begin{array}{l} r(n) < n \\ f(r(n)) < f (n) \\ \forall m < n, \textnormal{ if } f(m) < f(n) \textnormal{ then } f(m) \leq f(r(n)) \end{array} \right.

lemma r_prop (n : β„•) (hn : n > 1) : ( (r n ∈ Finset.range n) ∧ (f (r n) < f n) ∧ (βˆ€ m ∈ Finset.range n, f m < f n β†’ f m ≀ f (r n)) ) := n:β„•hn:n > 1⊒ r n ∈ Finset.range n ∧ f (r n) < f n ∧ βˆ€ m ∈ Finset.range n, f m < f n β†’ f m ≀ f (r n)

The result is symmetric for s and goes by the name s_prop.

Lemma 4.3πŸ”—

Let n > 1. Then either r(n) = 1 or r(n) > 1. That is, r(n) = 0 is impossible. Analogously, s(n) = 1 is impossible, hence either s(n) = 0 or s(n) > 1.

lemma r_options (n : β„•) (hn : n > 1) : r n = 1 ∨ r n > 1 := n:β„•hn:n > 1⊒ r n = 1 ∨ r n > 1lemma s_options (n : β„•) (hn : n > 1) : s n = 0 ∨ s n > 1 := n:β„•hn:n > 1⊒ s n = 0 ∨ s n > 1

We also obtain a result rs_options that encapsulates the four possible combinations of values for r and s, to make working with them easier.

Proof. If we had r(n) = 0, we would have 1 = f(0) = f(r(n)) < f(n), which is impossible since f takes values in [0, 1]. ∎

Lemma 4.4πŸ”—

Let n > 1 and suppose that s(n) > 1 and that r(n) < s(n). Then r(n) = r(s(n)).

Analogously, if r(n) >1 and s(n) < r(n), then s(n) = s(r(n)).

lemma rn_eq_rsn (n : β„•) (hn : n > 1) (hsn : s n > 1) (h : r n < s n) : r n = r (s n) := n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ r n = r (s n)

The analogue of this one goes by the name sn_eq_srn.

Proof. We prove only the first one; the second one is similar. Let n > 1 and suppose that s(n) > 1 and that r(n) < s(n). We want to see that r(n) = r(s(n)). By the injectivity of f, we can check instead that f (r (n)) = f (r (s (n))). Let us see that both inequalities hold.

n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f (r n) = f (r (s n)) n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f (r (s n)) ≀ f (r n)n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f (r n) ≀ f (r (s n))

(1) To see f (r (s (n))) \leq f (r (n)), we apply the third part of r_prop. So we have to see that r(s(n)) < n, which is easy since r(s(n)) < s(n) < n, and that f (r (s (n))) < f n. The latter is true because if we had f(n) < f(r(s(n))), since r(s(n)) < s(n) we would have f(s (n)) \leq f(r(s(n))), but that is impossible because f(r(s(n))) < f(s(n)) by construction (this last part is given by an auxiliary result f_rs_prop).

n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f (r (s n)) ≀ f (r n) -- f (r (s n)) ≀ f (r n) n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ r (s n) ∈ Finset.range nn:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f (r (s n)) < f n n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ r (s n) ∈ Finset.range n n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ r (s n) < n n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ r (s n) < s nn:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ s n < n n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ r (s n) < s n All goals completed! πŸ™ n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ s n < n All goals completed! πŸ™ n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f (r (s n)) < f n All goals completed! πŸ™

(2) To see that f (r (n)) \leq f (r (s (n))), it suffices to see that r(n) < s(n) by hypothesis and that f(r(n)) < f(n) < f(s(n)) by the properties of r and s. Then applying the third basic property to s(n) > 1 and r(n) < s(n) we obtain the result.

n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f (r n) ≀ f (r (s n)) -- f (r n) ≀ f (r (s n)) n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ r n ∈ Finset.range (s n)n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f (r n) < f (s n) n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ r n ∈ Finset.range (s n) All goals completed! πŸ™ n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f (r n) < f (s n) n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f (r n) < f nn:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f n < f (s n) n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f (r n) < f n All goals completed! πŸ™ n:β„•hn:n > 1hsn:s n > 1h:r n < s n⊒ f n < f (s n) All goals completed! πŸ™

∎

4.3.3.Β Construction of GπŸ”—

The construction of G : \mathbb{Q} \to \mathcal{P}(X) is, as we have explained, a construction by induction. To begin with, it is easier to construct G : \mathbb{N} \to \mathcal{P}(X), and afterwards take G \circ f^{-1} : Q \to \mathcal{P}(X) where f is the function numbering Q that we had obtained before.

Lean supports inductive definitions in a very natural way. A widely used example is the Fibonacci sequence: define Fib(0) = 0 and Fib(1) = 1, and from there, Fib(n) = Fib(n-1)+Fib(n-2) for each n > 1. In Lean, we write

def Fib : β„• β†’ β„• := fun n ↦ if n = 0 then 0 else if n = 1 then 1 else Fib (n-1) + Fib (n-2)

In view of this, my first approach to the construction of G was the following:

  • For n = 0, define G(0) = C_2^c.

  • For n = 1, take G(1) to be the result of applying the characterisation of normal spaces to the open set C_2^c and the closed set C_1.

  • For n >1, take G(n) to be the result of applying the characterisation of normal spaces (3.14) to the open set G(s(n)) and the closed set \overline{G(r(n))}.

  def G {X : Type} [TopologicalSpace X]
    (hT : βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’
      βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U)
    (C1 C2 : Set X) (hC1 : IsClosed C1)
    (hC2 : IsOpen C2ᢜ) (hC1C2 : C1 βŠ† C2ᢜ)
    : β„• β†’ Set X := fun n ↦
      if n = 0 then C2ᢜ
      else if n = 1 then Classical.choose (hT C2ᢜ C1 hC2 hC1 hC1C2)
      else
        let U := g hT C1 C2 hC1 hC2 hC1C2 (s n)
        let C := closure (g hT C1 C2 hC1 hC2 hC1C2 (r n))
        Classical.choose (hT U C (by sorry) (by sorry) (by sorry))

Where in the final sorrys we would have to prove that G(s(n)) is open, that \overline{G(r(n))} is closed and that \overline{G(r(n))} \subseteq G(s(n)), in order to be able to apply the characterisation of normality (hT).

All of this, we "know": it is the induction hypothesis. But we have not told Lean anything about it yet. How can we prove something about an object we have not defined yet, when we need to have proved it in order to define it?

To avoid this problem, I took a different strategy. First, I define the notion of a normal pair in the following way.

Definition 4.1πŸ”—

Given U, C \subseteq X, we say that (U, C) is a normal pair if U is open, C is closed and C \subseteq U. That is, if they satisfy the conditions needed to apply the characterisation of normal spaces (3.14).

def normal_pair {X : Type} [TopologicalSpace X] : (Set X Γ— Set X) β†’ Prop := fun (U, C) ↦ (IsOpen U ∧ IsClosed C ∧ C βŠ† U)

Now, I define a function from_normality that takes any two sets of X, and returns the result of applying the characterisation of normal spaces if they form a normal pair, and the empty set otherwise.

noncomputable def from_normality {X : Type} [T : TopologicalSpace X] (hT : βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U) : (Set X Γ— Set X) β†’ Set X := fun (U, C) ↦ if h : normal_pair (U, C) = True then Classical.choose (hT U C (X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† Ux✝:Set X Γ— Set XU:Set XC:Set Xh:normal_pair (U, C) = True⊒ IsOpen U X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† Ux✝:Set X Γ— Set XU:Set XC:Set Xh:normal_pair (U, C)⊒ IsOpen U; All goals completed! πŸ™) (X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† Ux✝:Set X Γ— Set XU:Set XC:Set Xh:normal_pair (U, C) = True⊒ IsClosed C X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† Ux✝:Set X Γ— Set XU:Set XC:Set Xh:normal_pair (U, C)⊒ IsClosed C; All goals completed! πŸ™) (X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† Ux✝:Set X Γ— Set XU:Set XC:Set Xh:normal_pair (U, C) = True⊒ C βŠ† U X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† Ux✝:Set X Γ— Set XU:Set XC:Set Xh:normal_pair (U, C)⊒ C βŠ† U; All goals completed! πŸ™) ) else βˆ…

Now, when constructing G, I no longer have to worry about whether it always produces open sets or not, because I can define it in terms of this last function, which is defined for any two sets. Once it is defined, I can prove that each set obtained is in fact open.

def G {X : Type} [T : TopologicalSpace X] (hT : βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U) (C1 C2 : Set X) : β„• β†’ Set X := fun n ↦ if n = 0 then C2ᢜ else if n = 1 then from_normality hT (C2ᢜ, C1) else if n > 1 then let U := G hT C1 C2 (s n) let C := closure (G hT C1 C2 (r n)) from_normality hT (U, C) else βˆ…

However, Lean is still not satisfied with this, and we receive this error: fail to show termination for G. That is, we are defining a recursive function, G, but it is not evident that the calls to G inside G refer to already-defined sets. In other words, it is not evident that r(n) < n and s(n) < n. Therefore, at the end of the definition we have to add a proof that this is indeed the case.

  ...
      else βˆ…

    decreasing_by
    Β· let s_prop := s_prop
      have aux : βˆ€ n > 1, s n < n
      Β· intro n hn
        specialize s_prop n hn
        simp at s_prop
        exact s_prop.left
      apply aux
      linarith
    Β· sorry -- analogo r

We have our function G! Although there is still a lot of work to do. Let us see that the properties we wanted from G hold.

Lemma 4.5πŸ”—

For each n \in \mathbb{N}, G(n) is open in X.

lemma G_Prop1 {X : Type} [T : TopologicalSpace X] (hT : βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U) (C1 C2 : Set X) (unused variable `hC1` Note: This linter can be disabled with `set_option linter.unusedVariables false`hC1 : IsClosed C1) (hC2 : IsOpen C2ᢜ) (unused variable `hC1C2` Note: This linter can be disabled with `set_option linter.unusedVariables false`hC1C2 : C1 βŠ† C2ᢜ) : βˆ€ n : β„•, IsOpen (G hT C1 C2 n) := X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜ⊒ βˆ€ (n : β„•), IsOpen (G hT C1 C2 n)

Proof. Note that the function from_normality always produces open sets, because either it is the result of applying 3.14, or it is the empty set, which is open (proved in from_normality_open).

Let n \in \mathbb{N}. We have to distinguish three cases, since there are three cases in the definition of G.

(1) If n = 0, then simply by hypothesis G(0) = C_2^c is open.

X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•βŠ’ IsOpen (G hT C1 C2 n) X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n = 0⊒ IsOpen (G hT C1 C2 n)X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 0⊒ IsOpen (G hT C1 C2 n) X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n = 0⊒ IsOpen (G hT C1 C2 n) -- n = 0 X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n = 0⊒ IsClosed C2 All goals completed! πŸ™

(2) If n = 1, then we are applying the function from_normality to C_2^c and C_1. Hence it is open.

X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 0this:n = 1 ∨ n > 1⊒ IsOpen (G hT C1 C2 n) X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 0hn1:n = 1⊒ IsOpen (G hT C1 C2 n)X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 0hn1:n > 1⊒ IsOpen (G hT C1 C2 n) X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 0hn1:n = 1⊒ IsOpen (G hT C1 C2 n) -- n = 1 X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 0hn1:n = 1⊒ IsOpen (if n = 0 then C2ᢜ else if n = 1 then from_normality hT (C2ᢜ, C1) else if n > 1 then have U := G hT C1 C2 (s n); have C := closure (G hT C1 C2 (r n)); from_normality hT (U, C) else βˆ…) X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 0hn1:n = 1⊒ IsOpen (from_normality hT (C2ᢜ, C1)) All goals completed! πŸ™

(3) Now, if n > 1, then we are applying the function from_normality to G(s(n)) and \overline{G(r(n))}. Hence it is open analogously. ∎

For the next result we are going to use complete induction. I have defined my own principle of complete induction, proved from the usual complete induction in Lean, for simplicity.

theorem my_stronger_induction (n : β„•) (P Q : β„• β†’ Prop) (hn : P n) (h : βˆ€ n : β„•, P n β†’ ((βˆ€ m < n, P m β†’ Q m) β†’ Q n)) : (Q n) := n:β„•P:β„• β†’ PropQ:β„• β†’ Prophn:P nh:βˆ€ (n : β„•), P n β†’ (βˆ€ m < n, P m β†’ Q m) β†’ Q n⊒ Q n

Lemma 4.6πŸ”—

For each n > 1, we have:

\overline{G(r(n))} \subseteq G(n) \subseteq \overline{G(n)} \subseteq G(s(n))

lemma G_Prop2 {X : Type} [T : TopologicalSpace X] (hT : βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U) (C1 C2 : Set X) (hC1 : IsClosed C1) (hC2 : IsOpen C2ᢜ) (hC1C2 : C1 βŠ† C2ᢜ) : βˆ€ n > 1, closure (G hT C1 C2 (r n)) βŠ† (G hT C1 C2 n) ∧ closure (G hT C1 C2 n) βŠ† (G hT C1 C2 (s n)) := X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜ⊒ βˆ€ n > 1, closure (G hT C1 C2 (r n)) βŠ† G hT C1 C2 n ∧ closure (G hT C1 C2 n) βŠ† G hT C1 C2 (s n)

Proof. We proceed by complete induction on n.

intro n X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 1⊒ closure (G hT C1 C2 (r n)) βŠ† G hT C1 C2 n ∧ closure (G hT C1 C2 n) βŠ† G hT C1 C2 (s n) X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 1P:β„• β†’ Prop := fun m => m > 1⊒ closure (G hT C1 C2 (r n)) βŠ† G hT C1 C2 n ∧ closure (G hT C1 C2 n) βŠ† G hT C1 C2 (s n) X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 1P:β„• β†’ Prop := fun m => m > 1⊒ P nX:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 1P:β„• β†’ Prop := fun m => m > 1⊒ βˆ€ (n : β„•), P n β†’ (βˆ€ m < n, P m β†’ closure (G hT C1 C2 (r m)) βŠ† G hT C1 C2 m ∧ closure (G hT C1 C2 m) βŠ† G hT C1 C2 (s m)) β†’ closure (G hT C1 C2 (r n)) βŠ† G hT C1 C2 n ∧ closure (G hT C1 C2 n) βŠ† G hT C1 C2 (s n) X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 1P:β„• β†’ Prop := fun m => m > 1⊒ βˆ€ (n : β„•), P n β†’ (βˆ€ m < n, P m β†’ closure (G hT C1 C2 (r m)) βŠ† G hT C1 C2 m ∧ closure (G hT C1 C2 m) βŠ† G hT C1 C2 (s m)) β†’ closure (G hT C1 C2 (r n)) βŠ† G hT C1 C2 n ∧ closure (G hT C1 C2 n) βŠ† G hT C1 C2 (s n) X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn:β„•hn:n > 1P:β„• β†’ Prop := fun m => m > 1⊒ βˆ€ (n : β„•), 1 < n β†’ (βˆ€ m < n, 1 < m β†’ closure (G hT C1 C2 (r m)) βŠ† G hT C1 C2 m ∧ closure (G hT C1 C2 m) βŠ† G hT C1 C2 (s m)) β†’ closure (G hT C1 C2 (r n)) βŠ† G hT C1 C2 n ∧ closure (G hT C1 C2 n) βŠ† G hT C1 C2 (s n) intro n X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn✝:β„•hn✝:n > 1P:β„• β†’ Prop := fun m => m > 1n:β„•hn:1 < n⊒ (βˆ€ m < n, 1 < m β†’ closure (G hT C1 C2 (r m)) βŠ† G hT C1 C2 m ∧ closure (G hT C1 C2 m) βŠ† G hT C1 C2 (s m)) β†’ closure (G hT C1 C2 (r n)) βŠ† G hT C1 C2 n ∧ closure (G hT C1 C2 n) βŠ† G hT C1 C2 (s n) X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn✝:β„•hn✝:n > 1P:β„• β†’ Prop := fun m => m > 1n:β„•hn:1 < nhi:βˆ€ m < n, 1 < m β†’ closure (G hT C1 C2 (r m)) βŠ† G hT C1 C2 m ∧ closure (G hT C1 C2 m) βŠ† G hT C1 C2 (s m)⊒ closure (G hT C1 C2 (r n)) βŠ† G hT C1 C2 n ∧ closure (G hT C1 C2 n) βŠ† G hT C1 C2 (s n)

We have the following induction hypothesis: for each m < n with m > 1 we have that \overline{G(r(m))} \subseteq G(m) \subseteq \overline{G(m)} \subseteq G(s(m)).

We want to see that then the same holds for n.

hi : βˆ€ m < n, 1 < m β†’ closure (G hT C1 C2 (r m)) βŠ† G hT C1 C2 m ∧ closure (G hT C1 C2 m) βŠ† G hT C1 C2 (s m)

⊒ closure (G hT C1 C2 (r n)) βŠ† G hT C1 C2 n ∧ closure (G hT C1 C2 n) βŠ† G hT C1 C2 (s n)

Note that if G(n) is obtained via 3.14 applied to G(s(n)) and \overline{G(r(n))}, the above reduces to checking that (G(s(n)), \overline{G(r(n))}) is a normal pair (proved in from_normality_prop2).

X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn✝:β„•hn✝:n > 1P:β„• β†’ Prop := fun m => m > 1n:β„•hn:1 < nhi:βˆ€ m < n, 1 < m β†’ closure (G hT C1 C2 (r m)) βŠ† G hT C1 C2 m ∧ closure (G hT C1 C2 m) βŠ† G hT C1 C2 (s m)aux:n β‰  0aux':n β‰  1U:Set X := G hT C1 C2 nU_def:U = from_normality hT (G hT C1 C2 (s n), closure (G hT C1 C2 (r n)))⊒ normal_pair (G hT C1 C2 (s n), closure (G hT C1 C2 (r n)))X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜn✝:β„•hn✝:n > 1P:β„• β†’ Prop := fun m => m > 1n:β„•hn:1 < nhi:βˆ€ m < n, 1 < m β†’ closure (G hT C1 C2 (r m)) βŠ† G hT C1 C2 m ∧ closure (G hT C1 C2 m) βŠ† G hT C1 C2 (s m)aux:n β‰  0aux':n β‰  1U:Set X := G hT C1 C2 nU_def:U = from_normality hT (G hT C1 C2 (s n), closure (G hT C1 C2 (r n)))normalpair:normal_pair (G hT C1 C2 (s n), closure (G hT C1 C2 (r n)))⊒ closure (G hT C1 C2 (r n)) βŠ† U ∧ closure U βŠ† G hT C1 C2 (s n)

We have seen that r(n) is either r(n) = 1 or r(n) > 1 (r_options) and s(n) is either s(n) = 0 or s(n) > 1 (s_options). Let us see, for example, the case r(n) = 1, s(n) > 1. The rest are similar and can be consulted in the repository.

(1) Seeing that G(s(n)) is open is easy; we have already seen that G always returns open sets.

  ...
    Β· exact G_Prop1 hT C1 C2 hC1 hC2 hC1C2 (s n)

(2) Seeing that \overline{G(r(n))} is closed is easy; we have already seen that the closure of any set is closed.

  ...
    Β· exact isClosed_closure

(3) Now, to see that \overline{G(r(n))} \subseteq G(s(n)), we need to use the induction hypothesis.

We know that s(n) < n. So we can apply the induction hypothesis to s(n), obtaining that

\overline{G(r(s(n)))} \subseteq G(s(n)) \subseteq \overline{G(s(n))} \subseteq G(s(s(n)))

But, since s(n) >1, we have that r(n) = r(s(n)) (rn_eq_rsn), obtaining \overline{G(r(n))} \subseteq G(s(n)).

  ...
    · have hsn := (s_prop n hn).left -- hsn : s n ∈ Finset.range n
      simp at hsn -- hsn : s n < n
      specialize hi (s n) hsn hs -- aplicar la H.I. a s(n)
      rw [rn_eq_rsn n hn hs (by linarith)] -- usar r(n) = r(s(n))
      exact hi.left

∎

4.3.4.Β The property (β˜…)πŸ”—

This is the most important property we want to require of the function G, since it is the one that guarantees the continuity of the function we want to construct for the proof of Urysohn's lemma, as we will see later.

Lemma 4.7πŸ”—

Let n, m \in \mathbb{N} with f(n) < f(m). Then

\overline{G(n)} \subseteq G(m)

lemma G_Prop2_ext {X : Type} [T : TopologicalSpace X] (hT : βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U) (C1 C2 : Set X) (hC1 : IsClosed C1) (hC2 : IsOpen C2ᢜ) (hC1C2 : C1 βŠ† C2ᢜ) : βˆ€ n m, f n < f m β†’ closure (G hT C1 C2 n) βŠ† G hT C1 C2 m := X:TypeT:TopologicalSpace XhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜ⊒ βˆ€ (n m : β„•), f n < f m β†’ closure (G hT C1 C2 n) βŠ† G hT C1 C2 m

To prove this result we are going to use a more general induction principle than the usual induction on the naturals. Whenever we have a well-founded relation on a set, an induction principle on that set can be described.

In our case, we are going to use the lexicographic order on \mathbb{N}^2, defined by (n, m) < (n', m') \iff n<n' \lor (n=n' \land m<m'). This is already defined in Mathlib, and it is also proved that it is a well-founded relation.

def lt_pair : (β„• Γ— β„•) β†’ (β„• Γ— β„•) β†’ Prop := Prod.Lex (Nat.lt) (Nat.lt) Definition `lt_pair_wfr` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`def lt_pair_wfr : WellFoundedRelation (β„• Γ— β„•) := Prod.lex (Nat.lt_wfRel) (Nat.lt_wfRel) lemma lt_pair_wf : WellFounded lt_pair := lt_pair_wfr.wf

Proof. We proceed, therefore, by well-founded induction on the pair (n, m)

    := by
  ... -- ciertas modificaciones del objetivo
  apply WellFounded.induction lt_pair_wf
  ...
  intro n m
  intro hi hnm

We therefore have the following induction hypothesis:

  hi : βˆ€ (a b : β„•), lt_pair (a, b) (n, m) β†’ f a < f b β†’ closure (G hT C1 C2 a) βŠ† G hT C1 C2 b

Now we split into different cases of values of n and m. We focus on the case n >1, m>1, which is the most interesting one, and the rest can be consulted in the repository.

Moreover, there are three possible cases: either f(s(n)) < f(m), or f(s(n)) = f(m), or f(s(n)) > f(m).

(1) If f(s(n)) < f(m), we have on the one hand that \overline{G(s(n))} \subseteq G(m), since (s(n), m) < (n, m) and the induction hypothesis.

On the other hand, \overline{G(n)} \subseteq G(s(n)), by the second property of G. So we have

\overline{G(n)} \subseteq G(s(n)) \subseteq \overline{G(s(n))} \subseteq G(m)

  ...
    Β· -- si f (s n) < f m
      trans closure (G hT C1 C2 (s n))
      Β· trans G hT C1 C2 (s n)
        Β· exact (G_Prop2 n hn1).right
        Β· exact subset_closure
      Β· exact hi (s n) m (by left; exact s_prop.left) h

(2) If f(s(n)) = f(m) it is very easy, because then by the injectivity of f we have s(n)= m, and \overline{G(n)} \subseteq G(s(n)) = G(m) by the second property of G.

  ...
    Β· -- si f (s n) = f m
      apply f_prop.left.left at h
      rw [h]
      exact (G_Prop2 n hn1).right

(3) Suppose now that f(s(n))>f(m). This is the most complicated case, and it requires splitting again into three possible options for f(n) \sim f(r(m)).

If f(n) < f(r(m)), we proceed in a similar way to (1), using the induction hypothesis for (n, r(m)) < (n, m). If f(n) = f(r(m)), we do the same as in (2). Finally, it remains to prove that f(r(m)) < f(n) cannot happen.

Indeed, if f(s(n))>f(m), it must be that n < m, because if we had m<n we would have f(n) < f(m) < f(s(n)), which is impossible by the properties of s. But then, if we had f(r(m)) < f(n) we would have f(r(m)) < f(n) < f(m) with n < m, which is impossible by the properties of r.

  ...
    Β· -- si f (r m) < f n
      by_contra
      have r_prop := r_prop.right.right n n_lt_m hnm -- f n ≀ f (r m)
      apply not_lt.mpr at r_prop -- Β¬f (r m) < f n
      exact r_prop h' -- teniamos h' : f (r m) < f n

∎

4.3.5.Β Composition with f^{-1}πŸ”—

Finally, let us remember that the function G we were looking for is not of the form \mathbb{N} \to \mathcal{P}(X) but of the form \mathbb{Q} \cap [0, 1] \to \mathcal{P}(X). In particular, we are going to extend it to \mathbb{Q} \to \mathcal{P}(X) in the following way:

H : \mathbb{Q} \to \mathcal{P}(X), ~~ q \mapsto \begin{cases} \emptyset & \text{if } q < 0 \\ (G \circ f^{-1})(q) & \text{if } 0 \leq q \leq 1 \\ X & \text{if } 1 < q \end{cases}

def H {X : Type} [TopologicalSpace X] (hT : βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U) (C1 C2 : Set X) : β„š β†’ Set X := fun q ↦ if q < 0 then βˆ… else if h : 0 ≀ q ∧ q ≀ 1 then G hT C1 C2 (f_inv ⟨q, h⟩) else Set.univ

Lemma 4.8πŸ”—

For the closed sets C_1 and C_2 chosen at the beginning of the section, the previously defined function H satisfies the following properties:

  1. H(1) = C_2^c

  2. H(0) is such that C_1 \subseteq H(0) \subseteq \overline{H(0)} \subseteq C_2^c

  3. For each q \in \mathbb{Q}, H(q) is open in X.

  4. For each p, q \in \mathbb{Q} with p < q, we have \overline{H(p)} \subseteq H(q)

Proof. All these properties follow almost trivially from those of G, using that f is bijective and the fixed values it takes at 0 and 1. The only addition is the values outside [0, 1], for which the last properties are proved easily since \emptyset and X are open, \overline{\emptyset} = \emptyset \subseteq U for any U and U \subseteq X for any U. ∎