compactness and `⋃ (i : β) (H : i ∈ b)`

Stream: maths

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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]

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