English
The closure of a preperfect set is a perfect set.
Русский
Замыкание предперфектного множества является совершенным.
LaTeX
$$$\text{Perfect}(C) \Leftarrow \text{Preperfect}(C) \Rightarrow \text{Perfect}(\overline{C}).$$$
Lean4
/-- The closure of a preperfect set is perfect.
For a converse, see `preperfect_iff_perfect_closure`. -/
theorem perfect_closure (hC : Preperfect C) : Perfect (closure C) :=
by
constructor; · exact isClosed_closure
intro x hx
by_cases h : x ∈ C <;> apply AccPt.mono _ (principal_mono.mpr subset_closure)
· exact hC _ h
have : { x }ᶜ ∩ C = C := by simp [h]
rw [AccPt, nhdsWithin, inf_assoc, inf_principal, this]
rw [closure_eq_cluster_pts] at hx
exact hx
