The Lebesgue number lemma for neighbourhood covers #
Mathlib's lebesgue_number_lemma_of_metric is stated for a cover of a compact set by open sets.
This file records the variant for a family of sets such that every point of the compact set has
some member of the family as a neighbourhood, as happens for the preimages of such a cover under
a continuous map.
Main declarations #
TauCeti.lebesgue_number_lemma_of_metric_of_mem_nhds: a Lebesgue number for a family of sets one of which is a neighbourhood of each point of a compact set.
theorem
TauCeti.lebesgue_number_lemma_of_metric_of_mem_nhds
{α : Type u_1}
{ι : Type u_2}
[PseudoMetricSpace α]
{s : Set α}
{c : ι → Set α}
(hs : IsCompact s)
(hc : ∀ x ∈ s, ∃ (i : ι), c i ∈ nhds x)
:
∃ δ > 0, ∀ x ∈ s, ∃ (i : ι), Metric.ball x δ ⊆ c i
A Lebesgue number for a family of sets c such that every point of the compact set s has
some c i as a neighbourhood: there is δ > 0 such that the ball of radius δ around any point
of s is contained in some c i.