## Stream: maths

### Topic: compactness and ⋃ (i : β) (H : i ∈ b)

#### Kevin Buzzard (Nov 09 2019 at 11:30):

Whilst thinking about this I realised that I couldn't find the version of "compact" which I wanted. I might naively say now "...and this is obviously the correct version of compactness which mathematicians use" but I might be blinded by the fact that it's the one I want now.

In the library we seem to have

compact_iff_finite_subcover :
∀ {α : Type u_1} [_inst_1 : topological_space α] {s : set α},
compact s ↔
∀ (c : set (set α)),
(∀ (t : set α), t ∈ c → is_open t) →
s ⊆ ⋃₀ c → (∃ (c' : set (set α)) (H : c' ⊆ c), set.finite c' ∧ s ⊆ ⋃₀ c')

compact_elim_finite_subcover :
∀ {α : Type u_1} [_inst_1 : topological_space α] {s : set α} {c : set (set α)},
compact s →
(∀ (t : set α), t ∈ c → is_open t) →
s ⊆ ⋃₀ c → (∃ (c' : set (set α)) (H : c' ⊆ c), set.finite c' ∧ s ⊆ ⋃₀ c')

compact_elim_finite_subcover_image :
∀ {α : Type u_1} {β : Type u_2} [_inst_1 : topological_space α] {s : set α} {b : set β} {c : β → set α},
compact s →
(∀ (i : β), i ∈ b → is_open (c i)) →
(s ⊆ ⋃ (i : β) (H : i ∈ b), c i) →
(∃ (b' : set β) (H : b' ⊆ b), set.finite b' ∧ s ⊆ ⋃ (i : β) (H : i ∈ b'), c i)


The first two are the usual type theory thing where people for some reason want sets of stuff instead of stuff indexed by a type. The third one, compact_elim_finite_subcover_image, has an index type β but then the cover of s is not by all the sets c i for i : β, there is this extra variable b, we cover s by the elements corresponding to b and so we have to work with this ⋃ (i : β) (H : i ∈ b') thing. Here H is a Prop and in particular a subsingleton.

What I want, today at least, is the more straightforward

example {α : Type*} {β : Type*} [topological_space α] {s : set α} {c : β → set α} :
compact s →
(∀ (i : β), is_open (c i)) →
(s ⊆ ⋃ (i : β), c i) →
(∃ (b' : finset β), s ⊆ ⋃ (i : β) (H : i ∈ b'), c i)
:= sorry


So no superfluous b (it is superfluous, one can just replace beta with b), and I've thrown in a finset for good measure rather than a set plus the assumption that it's finite. Furthermore this approach removes one of the ⋃ (i : β) (H : i ∈ b) things which are somehow a pain to work with (until one discovers set.Union_pos).

In fact I guess this is an iff. Should this example be in mathlib or is there some infinite list of variants which we can't hope to capture and I'm supposed to just get on with it and work with what we have?

#### Reid Barton (Nov 09 2019 at 15:37):

I would suggest trying to replace the existing uses of compact_elim_finite_subcover_image (and possibly also compact_elim_finite_subcover) with your variant and see whether the proofs get easier, harder, or not much different.

#### Kevin Buzzard (Nov 09 2019 at 17:30):

I might not do this for a while because I really want to release a new natnumgame this weekend but I will come back to this.

#### Mario Carneiro (Nov 09 2019 at 18:56):

Yeah, your version looks better. The existing one is too much set theory

#### Kevin Buzzard (Nov 09 2019 at 19:18):

@Patrick Massot I'd be interested to hear your comments at some point.

#### Patrick Massot (Nov 11 2019 at 13:42):

There are two different issues here. The first one is finset vs finite. I don't have a strong opinion about which one is better, but clearly going back and forth is painful. If we want to keep both then we probably need to duplicate compactness lemmas. The second issue of indexing by a type or a subset of a type. I agree that indexing by a full type sounds simpler, and can emulate the more specialized version.

#### Patrick Massot (Nov 11 2019 at 13:49):

For reference I proved a couple of versions of the statement from the original discussion.

import topology.metric_space.basic

open set metric

lemma kevin_compact {α : Type*} {β : Type*} [topological_space α] {s : set α} {c : β → set α} :
compact s →
(∀ (i : β), is_open (c i)) →
(s ⊆ ⋃ (i : β), c i) →
(∃ (b' : finset β), s ⊆ ⋃ (i : β) (H : i ∈ b'), c i) :=
begin
intros s_comp c_op s_sub,
obtain ⟨t, t_sub, t_fin, h⟩ : ∃ t ⊆ range c, finite t ∧ s ⊆ ⋃₀ t,
from compact_elim_finite_subcover s_comp (by { rintros _ ⟨_, rfl⟩, tauto }) s_sub,
obtain ⟨u, rfl, hu⟩ : ∃ (u : set β), t = c '' u ∧ inj_on c u,
from (subset_range_iff c).mp t_sub,
have u_fin : finite u,
from (finite_image_iff_on hu).mp t_fin,
use u_fin.to_finset,
intros x x_in,
rcases h x_in with ⟨_, ⟨b, b_in, rfl⟩, x_in_cb⟩,
rw mem_Union,
use b,
simpa [b_in] using x_in_cb
end

variables {X : Type*} [metric_space X] {O : X} (Hcomp : compact (closed_ball O 1))
{r : ℝ} (hr : r > 0)

include Hcomp hr

-- Version 1: finite instead of finset, uses mathlib's compact_elim_finite_subcover_image
example : ∃ A : set X, finite A ∧ ∀ x ∈ closed_ball O 1, ∃ a ∈ A, dist x a ≤ r :=
begin
have cover : closed_ball O 1 ⊆ ⋃ a ∈ closed_ball O 1, ball a r,
{ intros x hx,
rw mem_Union,
use x,
simpa [mem_Union, hx, hr] },
obtain ⟨A, A_sub, A_fin, h⟩ :
∃ A ⊆ closed_ball O 1, finite A ∧ closed_ball O 1 ⊆ ⋃ a ∈ A, ball a r,
from compact_elim_finite_subcover_image Hcomp (by simp[is_open_ball]) cover,
use [A, A_fin],
assume x (x_in : x ∈ closed_ball O 1),
obtain ⟨a, a_in, ha⟩ : ∃ a ∈ A, dist x a < r,
by simpa using h x_in,
use [a, a_in],
linarith
end

-- Version 2: finset instead of finite (note the need for finite.to_finset),
-- uses mathlib's compact_elim_finite_subcover_image
example : ∃ A : finset X, ∀ x ∈ closed_ball O 1, ∃ a ∈ A, dist x a ≤ r :=
begin
have cover : closed_ball O 1 ⊆ ⋃ a ∈ closed_ball O 1, ball a r,
{ intros x hx,
rw mem_Union,
use x,
simpa [mem_Union, hx, hr] },
obtain ⟨A, A_sub, A_fin, h⟩ :
∃ A ⊆ closed_ball O 1, finite A ∧ closed_ball O 1 ⊆ ⋃ a ∈ A, ball a r,
from compact_elim_finite_subcover_image Hcomp (by simp[is_open_ball]) cover,
use A_fin.to_finset,
assume x (x_in : x ∈ closed_ball O 1),
obtain ⟨a, a_in, ha⟩ : ∃ a ∈ A, dist x a < r,
by simpa using h x_in,
simp,
use [a, a_in],
linarith
end

-- Version 3: finset instead of finite,
-- uses Kevin's version of compact_elim_finite_subcover_image
-- (no need for finite.to_finset since both the example and Kevin lemma use only finsets)
example : ∃ A : finset X, ∀ x ∈ closed_ball O 1, ∃ a ∈ A, dist x a ≤ r :=
begin
have cover : closed_ball O 1 ⊆ ⋃ a : X, ball a r,
{ intros x hx,
rw mem_Union,
use x,
simpa [mem_Union, hx, hr] },
obtain ⟨A, Asub⟩ :
∃ (A : finset X), closed_ball O 1 ⊆ ⋃ (i : X) (H : i ∈ A), (λ (a : X), ball a r) i,
from kevin_compact Hcomp (by simp[is_open_ball]) cover,
use A,
assume x (x_in : x ∈ closed_ball O 1),
obtain ⟨a, a_in, ha⟩ : ∃ a ∈ A, dist x a < r,
by simpa using Asub x_in,
use [a, a_in],
linarith
end


Last updated: May 12 2021 at 07:17 UTC