Lebesgues_Number_Lemma
Provedcompactnessmetric-spacesproofwiki
Let M = (A, d) be a compact metric space. Then there exists a Lebesgue number for every open cover of M.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Lebesgues_Number_Lemma {X : Type _} [MetricSpace X] [CompactSpace X] (C : Set (Set X)) (hC : ∀ U ∈ C, IsOpen U) (hCov : ⋃₀ C = Set.univ) : ∃ δ > 0, ∀ x : X, ∃ U ∈ C, Metric.ball x δ ⊆ U := by sorrySource