exists_inter_eq_singleton_of_mem_discrete

English

Let nhds x have a basis (p t). If x ∈ s with s discrete, there exists an index i with p(i) and t(i) ∩ s = {x}.

Русский

Пусть у окрестностей x есть базис (p i, t i). Если x ∈ s и s дискретно, существует индекс i, для которого p(i) и t(i) ∩ s = {x}.

LaTeX

$$$ (\\nhds x).HasBasis(p,t) \\rightarrow x \\in s \\rightarrow \\exists i, p(i) \\wedge t(i) \\cap s = \\{x\\}. $$$

Lean4

theorem exists_inter_eq_singleton_of_mem_discrete {ι : Type*} {p : ι → Prop} {t : ι → Set X} {s : Set X}
    [DiscreteTopology s] {x : X} (hb : (𝓝 x).HasBasis p t) (hx : x ∈ s) : ∃ i, p i ∧ t i ∩ s = { x } :=
  by
  rcases (nhdsWithin_hasBasis hb s).mem_iff.1 (singleton_mem_nhdsWithin_of_mem_discrete hx) with ⟨i, hi, hix⟩
  exact ⟨i, hi, hix.antisymm <| singleton_subset_iff.2 ⟨mem_of_mem_nhds <| hb.mem_of_mem hi, hx⟩⟩

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