Positive overlap

Stream: Is there code for X?

[Vincent Beffara]

Do we have this somewhere? (Possibly in much larger generality like a uniform space?)

import Mathlib

variable {K : Set ℝ} {S : Finset (Set ℝ)}

lemma bla (hK : IsCompact K) (hS : ∀ s ∈ S, IsOpen s) (hKS : K ⊆ ⋃ s ∈ S, s) :
    ∃ ε > 0, ∀ x ∈ K, ∃ s ∈ S, closedBall x ε ⊆ s := by
  sorry

[Sebastien Gouezel]

Something like docs#lebesgue_number_lemma, maybe?

[Vincent Beffara]

Yes exactly! Thanks!

[Sebastien Gouezel]

There is now a very cool way to find the anwer to this kind of question: ask loogle to state all theorems mentioning all the stuff that should be in your statements.

[Sebastien Gouezel]

@loogle IsCompact, IsOpen, Set, (∃ _, _), (⋃ _, _)

[loogle]

:search: isCompact_iff_finite_subcover, isCompact_of_finite_subcover, and 12 more

[Sebastien Gouezel]

I've been pretty vague in my query since it wasn't clear if it would be in metric or uniformity terms, but for sure there would be an existential, a union, and IsCompact, IsOpen and Set.

[Sebastien Gouezel]

And I notice in the suggestions by loogle a better answer to your question: docs#lebesgue_number_lemma_of_metric

[Vincent Beffara]

Yes I just saw it. It is just stated in terms of an indexed family instead of a set of sets, which I guess is why exact? was not helping.

[Vincent Beffara]

It's kind of amazing that loogle works that well (I would have expected a much longer list of lemmas with that request ...)