lebesgue_number_lemma_of_emetric_nhdsWithin'

English

Lebesgue number lemma for nhdsWithin' setting: compact s and function c yields δ > 0 with ball intersections contained in c.

Русский

Лемма числа Лебега для nhdsWithin' области: компактное s и отображение c дают δ > 0 с пересечениями шаров, входящих в c.

LaTeX

$$lebesgue_number_lemma_nhdsWithin' hs hc$$

Lean4

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

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