lebesgue_number_lemma_of_emetric_sUnion

English

Lebesgue number lemma for a union of sets; given IsCompact s and a family c of open sets, there exists δ > 0 with ball x δ contained in some member of the family.

Русский

Лемма числа Лебега для объединения множеств; при компактности s и семейства открытых множеств существует δ > 0 такое, что круглый шар вокруг любого x ⊆ s содержится в некотором элементе семейства.

LaTeX

$$lebesgue_number_lemma_of_emetric_sUnion hs hc₁ hc₂$$

Lean4

theorem lebesgue_number_lemma_of_emetric_sUnion {c : Set (Set α)} (hs : IsCompact s) (hc₁ : ∀ t ∈ c, IsOpen t)
    (hc₂ : s ⊆ ⋃₀ c) : ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t := by rw [sUnion_eq_iUnion] at hc₂;
  simpa using lebesgue_number_lemma_of_emetric hs (by simpa) hc₂

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