lebesgue_number_lemma_of_emetric_nhds'

English

Lebesgue number lemma in the nhds' topology setting: given compact s and a family of sets c defined by neighborhoods, there exists δ > 0 such that ...

Русский

Лебегов номер в окружении nhds' : при компактности s существует δ > 0 такое, что ...

LaTeX

$$lebesgue_number_lemma_nhds' hs hc$$

Lean4

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

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