exists_mem_nhds_ball_subset_of_mem_nhds

English

Given a compact K and a family U(x) of neighborhoods with x ∈ K, there is a V in the uniformity so that around every x ∈ K there is a y ∈ K with ball x V ⊆ U(y).

Русский

Пусть K компактно и есть семейство окрестностей U(x) для каждого x ∈ K; существует V из равномерности так, что для каждого x ∈ K найдётся y ∈ K с ball x V ⊆ U(y).

LaTeX

$$$ \forall K : Set α, IsCompact K \to\ (\forall x hx, U x hx ∈ 𝓝 x) \to\exists V ∈ 𝓤 α, \forall x \in K, \exists y : K, ball x V ⊆ U y y.2$$$

Lean4

theorem exists_mem_nhds_ball_subset_of_mem_nhds {a : α} {U : Set α} (h : U ∈ 𝓝 a) :
    ∃ V ∈ 𝓝 a, ∃ t ∈ 𝓤 α, ∀ a' ∈ V, UniformSpace.ball a' t ⊆ U :=
  let ⟨t, ht, htU⟩ := comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 h)
  ⟨_, mem_nhds_left a ht, t, ht, fun a₁ h₁ a₂ h₂ => @htU (a, a₂) ⟨a₁, h₁, h₂⟩ rfl⟩

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