lebesgue_number_lemma_of_metric_sUnion

English

If s is compact and c is a collection of open sets with s ⊆ ⋃ c, then there exists δ>0 such that for each x ∈ s, there exists a set t in c with ball x δ ⊆ t.

Русский

Если s компактно и имеется семейство открытых множеств c, удовлетворяющее s ⊆ ⋃ c, тогда существует δ>0 такое, что для каждой x∈s существует т∈c с B(x,δ) ⊆ t.

LaTeX

$$$\text{IsCompact}(s) \rightarrow (\forall t\in c, \ IsOpen(t)) \rightarrow s \subseteq \bigcup_{t\in c} t \rightarrow \exists \delta>0, \forall x\in s, \exists t\in c, \mathrm{ball}(x,\delta) \subseteq t$$$

Lean4

theorem lebesgue_number_lemma_of_metric_sUnion {s : Set α} {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_metric hs (by simpa) hc₂

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