mem_closure_iff_nhds_basis' — Mathlib

English

If 𝓝 x has a basis {s_i} with property p_i, then x ∈ closure t iff ∀ i, p_i implies s_i ∩ t ≠ ∅.

Русский

Если у 𝓝 x есть базис {s_i} с свойством p_i, то x ∈ closure t тогда и только тогда, когда для всех i, если p_i, то s_i ∩ t ≠ ∅.

LaTeX

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

Lean4

theorem mem_closure_iff_nhds_basis' {p : ι → Prop} {s : ι → Set X} (h : (𝓝 x).HasBasis p s) :
    x ∈ closure t ↔ ∀ i, p i → (s i ∩ t).Nonempty :=
  mem_closure_iff_clusterPt.trans <| (h.clusterPt_iff (hasBasis_principal _)).trans <| by simp only [forall_const]

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