mem_closure_iff_nhds_basis — Mathlib

English

If 𝓝 x has a basis {s_i}, then x ∈ closure t iff ∀ i, p_i → ∃ y ∈ t with y ∈ s_i.

Русский

Если 𝓝 x имеет базис {s_i}, то x ∈ closure t тогда и только тогда, когда ∀ i, p_i → ∃ y ∈ t с y ∈ s_i.

LaTeX

$$$(\mathcal{N}x).HasBasis\ p\ s \Rightarrow x \in \overline{t} \iff \forall i,\ p_i \Rightarrow \exists y \in t,\ y \in s_i$$$

Lean4

theorem mem_closure_iff_nhds_basis {p : ι → Prop} {s : ι → Set X} (h : (𝓝 x).HasBasis p s) :
    x ∈ closure t ↔ ∀ i, p i → ∃ y ∈ t, y ∈ s i :=
  (mem_closure_iff_nhds_basis' h).trans <| by simp only [Set.Nonempty, mem_inter_iff, and_comm]

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