lebesgue_number_lemma_nhdsWithin'

English

Analogous to Lebesgue number lemma but with nhdsWithin: compact K and a family U x hx within K have a uniform radius V to fit inside U y for some y ∈ K.

Русский

Аналогично лемме Лебега для nhdsWithin: компактное K и семейство U x hx внутри K имеют общий радиус V, чтобы шар x V попал в U y для некоторого y ∈ K.

LaTeX

$$$\exists V \in 𝓤(\alpha),\; \forall x\in K,\; \exists y\in K,\; B(x,V) \cap K \subseteq U y$$$

Lean4

theorem lebesgue_number_lemma_nhdsWithin' {U : (x : α) → x ∈ K → Set α} (hK : IsCompact K)
    (hU : ∀ x hx, U x hx ∈ 𝓝[K] x) : ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y : K, ball x V ∩ K ⊆ U y y.2 :=
  (lebesgue_number_lemma_nhds' hK (fun x hx => Filter.mem_inf_principal'.1 (hU x hx))).imp fun _ ⟨V_uni, hV⟩ =>
    ⟨V_uni, fun x hx => (hV x hx).imp fun _ hy => (inter_subset _ _ _).2 hy⟩

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