lebesgue_number_lemma_of_emetric — Mathlib

English

For a compact set s and an open cover {c i}, there exists δ > 0 such that every x ∈ s lies in some ball B(x, δ) contained in some c i.

Русский

Для компактного множества s и открытого покрытия {c i} существует δ > 0, такое что каждый x ∈ s принадлежит шарy B(x, δ), содержащемуся в некотором c i.

LaTeX

$$IsCompact s → (∀ i, IsOpen (c i)) → s ⊆ ⋃ i, c i → ∃ δ > 0, ∀ x ∈ s, ∃ i, ball x δ ⊆ c i$$

Lean4

theorem lebesgue_number_lemma_of_emetric {ι : Sort*} {c : ι → Set α} (hs : IsCompact s) (hc₁ : ∀ i, IsOpen (c i))
    (hc₂ : s ⊆ ⋃ i, c i) : ∃ δ > 0, ∀ x ∈ s, ∃ i, ball x δ ⊆ c i := by
  simpa only [ball, UniformSpace.ball, preimage_setOf_eq, edist_comm] using
    uniformity_basis_edist.lebesgue_number_lemma hs hc₁ hc₂

Похожие утверждения