lebesgue_number_lemma_of_emetric_nhdsWithin

English

Lebesgue number lemma for nhdsWithin: for compact s and open cover of s by balls, there exists δ > 0 with ball x δ contained in some cover element for all x in s.

Русский

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

LaTeX

$$lebesgue_number_lemma_of_emetric_nhdsWithin hs hc$$

Lean4

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

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