disjoint covers of compacts

Stream: new members

[Christian Merten]

Is there something like "If a compact set in a topological space is covered by pairwise disjoint opens, the covering is finite." in mathlib? I tried to loogle, but without success.

[Michael Rothgang]

docs#IsCompact.elim_finite_subcover should do what you want

[Michael Rothgang]

(Disjointness of the open sets is not required.)

[Patrick Massot]

Michael, I think you read too quickly Christian's statement.

[Patrick Massot]

Of course it will follow from the lemma you quoted, and I'm pretty confident Christian knows this, he simply want to know whether this result is already there.

[Michael Rothgang]

Patrick Massot said:

Of course it will follow from the lemma you quoted, and I'm pretty confident Christian knows this, he simply want to know whether this result is already there.

Ah, right. Indeed, I was too hasty. I should go to bed :-)

[Christian Merten]

So I suppose the answer is: It is not there yet?

[Christian Merten]

Is this the right way to state this?

import Mathlib.Topology.SubsetProperties

universe v

variable {α : Type*} [TopologicalSpace α] [CompactSpace α]

example {ι : Type v} (U : ι → Set α) (hUo : ∀ i, IsOpen (U i))
    (hsU : Set.univ ⊆ ⋃ i, U i) (hdU : ∀ i j, i ≠ j → Disjoint (U i) (U j))
    (hnU : ∀ i, (U i).Nonempty) : Finite ι :=
  sorry

I formulated it for the whole space, otherwise one would have to say something like:

variable {α : Type*} [TopologicalSpace α]

example {ι : Type v} {s : Set α} (hs : IsCompact s)
    (U : ι → Set α) (hUo : ∀ i, IsOpen (U i)) (hsU : s ⊆ ⋃ i, U i)
    (hdU : ∀ i j, i ≠ j → Disjoint (U i ∩ s) (U j ∩ s))
    (hnU : ∀ i, (U i ∩ s).Nonempty) : Finite ι := sorry

which feels very clumsy.