nhdset_of_mem_uniformity — Mathlib

English

An equivalent formulation: a countable antitone basis with symmetric entourages exists for 𝓤 α.

Русский

Эквивалентная формулировка: существует счётная антонычная база с симметричными окружностями для 𝓤 α.

LaTeX

$$$\\exists V,\\ HasAntitoneBasis(\\mathcal{U}α, V) \\land \\forall n, IsSymmetricRel(V(n))$$$

Lean4

theorem nhdset_of_mem_uniformity {d : Set (α × α)} (s : Set (α × α)) (hd : d ∈ 𝓤 α) :
    ∃ t : Set (α × α), IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d} :=
  by
  let cl_d := {p : α × α | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
  have : ∀ p ∈ s, ∃ t, t ⊆ cl_d ∧ IsOpen t ∧ p ∈ t := fun ⟨x, y⟩ hp =>
    mem_nhds_iff.mp <|
      show cl_d ∈ 𝓝 (x, y) by
        rw [nhds_eq_uniformity_prod, mem_lift'_sets]
        · exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩
        · exact fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩
  choose t ht using this
  exact
    ⟨(⋃ p : α × α, ⋃ h : p ∈ s, t p h : Set (α × α)),
      isOpen_iUnion fun p : α × α => isOpen_iUnion fun hp => (ht p hp).right.left, fun ⟨a, b⟩ hp => by
      simp only [mem_iUnion, Prod.exists]; exact ⟨a, b, hp, (ht (a, b) hp).right.right⟩,
      iUnion_subset fun p => iUnion_subset fun hp => (ht p hp).left⟩

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