lebesgue_number_lemma_of_emetric_nhds

English

Lebesgue number lemma in the nhds topology: For compact s and a cover by sets c x, there exists δ > 0 such that every x ∈ s is contained in some ball B(x, δ) inside some c y.

Русский

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

LaTeX

$$lebesgue_number_lemma_of_emetric_nhds hs hc$$

Lean4

theorem lebesgue_number_lemma_of_emetric_nhds {c : α → Set α} (hs : IsCompact s) (hc : ∀ x ∈ s, c x ∈ 𝓝 x) :
    ∃ δ > 0, ∀ x ∈ s, ∃ y, ball x δ ⊆ c y := by
  simpa only [ball, UniformSpace.ball, preimage_setOf_eq, edist_comm] using
    uniformity_basis_edist.lebesgue_number_lemma_nhds hs hc

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