Compactness in Metric Spaces

Stream: new members

[Nelitha Kulasiri]

Hello! I am currently writing a proof in lean for the following,

theorem ClosedBounded (S : Set X): compact S → Closed S ∧ Bounded S

where I have written my own definitions for compact, closed, and bounded.

def Open (S: Set X) := ∀x∈S, ∃r>0, (ball x r) ⊆ S
def Closed (S: Set X) := Open Sᶜ
def Bounded (S: Set X) := ∃r, ∃ x : X, S ⊆ ball x r
def Opencover (F: Set (Set X)) (S: Set X) := S ⊆ ⋃₀ F ∧ ∀f∈F, Open f
def finiteOpenCover (F: Set (Set X)) (S: Set X) := (Opencover F S) ∧ Finite F
def compact (S: Set X) := ∀ F, Opencover F S → ∃ G, G ⊆ F ∧ finiteOpenCover G S

I want to use the fact that the family of balls {B(x0,n)} covers S, for n in the naturals and some x0 in X (the metric space). However I am unsure how to specialize the F in the definition of compact to my sequence of sets. I am also a bit unsure on how to write such a sequence in lean. Any help would be appreciated, thanks!

[Ruben Van de Velde]

A sequence would probably be represented as a function from Nat to Set X

[Patrick Massot]

There are a couple of things that could help you. First you need to be more efficient at asking for help by reading the link #mwe, making sure people can copy-paste your code in an empty Lean file and start playing with it. In your case that would mean replacing your second snippet by

import Mathlib

variable {X : Type} [MetricSpace X]
open Metric Set Function

def Open (S: Set X) := ∀x∈S, ∃r>0, (ball x r) ⊆ S
def Closed (S: Set X) := Open Sᶜ
def Bounded (S: Set X) := ∃r, ∃ x : X, S ⊆ ball x r
def Opencover (F: Set (Set X)) (S: Set X) := S ⊆ ⋃₀ F ∧ ∀f∈F, Open f
def finiteOpenCover (F: Set (Set X)) (S: Set X) := (Opencover F S) ∧  Finite F
def compact (S : Set X) := ∀ F, Opencover F S → ∃ G, G ⊆ F ∧ finiteOpenCover G S

(of course you can replace import Mathlib by something more refined.

[Patrick Massot]

Then I think that Finite F is a typo, it should be Set.Finite F or F.Finite. They are equivalent, but the Set.Finite version is probably more convenient.

[Patrick Massot]

Then you need a lemma restating the compactness property for indexed unions. In the definition you need to choose between using set unions or indexed unions, but in proofs you need both. So you need something like:

lemma compact.finite_subcover {S : Set X} (hS : compact S) {ι: Type*} {F : ι → Set X}
    (hF : ∀ i, Open (F i)) (hSF : S ⊆ ⋃ i, F i) : ∃ I : Set ι, I.Finite ∧ S ⊆ ⋃ i ∈ I, F i

[Patrick Massot]

In order to prove that you will probably need answers to this question, but you can sorry those lemmas in the mean time.

[Patrick Massot]

Also, depending on what you want to do, I'm not sure that restricting to radii that are natural numbers will buy you anything but trouble with the coercion between Nat and Real.

[Nelitha Kulasiri]

Thank you!