preperfect_iff_nhds — Mathlib

English

In a topological space, a set C is preperfect if and only if every point x in C has every neighborhood U of x containing some y ≠ x with y ∈ C.

Русский

Во множестве C предперфектно тогда и только тогда, когда для каждого x ∈ C и любого окружения U x найдется y ≠ x с y ∈ C и y ∈ U.

LaTeX

$$$\text{Preperfect}(C) \iff \forall x\in C, \forall U\in \mathcal{N}(x), \exists y \in U \cap C, y \neq x.$$$

Lean4

theorem preperfect_iff_nhds : Preperfect C ↔ ∀ x ∈ C, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x := by
  simp only [Preperfect, accPt_iff_nhds]

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