English
A set is preperfect if every point of the set is an accumulation point of the set itself.
Русский
Множество предперфектно, если каждый его элемент является точкой накопления множества самого себя.
LaTeX
$$$ \text{Preperfect}(C) \;\equiv\; \forall x \in C, \ AccPt(x, \mathcal{P} C). $$$
Lean4
/-- If `x` is an accumulation point of a set `C` and `U` is a neighborhood of `x`,
then `x` is an accumulation point of `U ∩ C`. -/
theorem nhds_inter {x : α} {U : Set α} (h_acc : AccPt x (𝓟 C)) (hU : U ∈ 𝓝 x) : AccPt x (𝓟 (U ∩ C)) :=
by
have : 𝓝[≠] x ≤ 𝓟 U := by
rw [le_principal_iff]
exact mem_nhdsWithin_of_mem_nhds hU
rw [AccPt, ← inf_principal, ← inf_assoc, inf_of_le_left this]
exact h_acc
