clusterPt_iff — Mathlib

English

For bases hX of nhds x and hF of F, ClusterPt x F iff for all i,j with pX i and pF j, the intersection sX i ∩ sF j is nonempty.

Русский

Для баз hX и hF: ClusterPt x F эквивалентно тому, что для всех i,j с pX i и pF j множества sX i ∩ sF j непусты.

LaTeX

$$$\operatorname{ClusterPt} x F \\iff \\forall i, pX i \\to \\forall j, pF j \\to (sX i \\cap sF j) \\neq \\emptyset$$$

Lean4

theorem clusterPt_iff {ιX ιF} {pX : ιX → Prop} {sX : ιX → Set X} {pF : ιF → Prop} {sF : ιF → Set X} {F : Filter X}
    (hX : (𝓝 x).HasBasis pX sX) (hF : F.HasBasis pF sF) :
    ClusterPt x F ↔ ∀ ⦃i⦄, pX i → ∀ ⦃j⦄, pF j → (sX i ∩ sF j).Nonempty :=
  hX.inf_basis_neBot_iff hF

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