English
If U is a nontrivial open-closed-like set in a T1-space under preconnectedness, then U is preperfect.
Русский
Если U ненулевой, подобный открытое-замыканию множество внутри T1-пространства и является предсоединенным, то U предперфектно.
LaTeX
$$$[T1Space \ α] \; (hu : U.Nontrivial) \; (h : IsPreconnected U) \Rightarrow \text{Preperfect } U.$$$
Lean4
theorem preperfect_of_nontrivial [T1Space α] {U : Set α} (hu : U.Nontrivial) (h : IsPreconnected U) : Preperfect U :=
by
intro x hx
rw [isPreconnected_closed_iff] at h
specialize h { x } (closure (U \ { x })) isClosed_singleton isClosed_closure ?_ ?_ ?_
· trans { x } ∪ (U \ { x })
· simp
apply Set.union_subset_union_right
exact subset_closure
· exact Set.inter_singleton_nonempty.mpr hx
· obtain ⟨y, hy⟩ := Set.Nontrivial.exists_ne hu x
use y
simp only [Set.mem_inter_iff, hy, true_and]
apply subset_closure
simp [hy]
· apply Set.Nonempty.right at h
rw [Set.singleton_inter_nonempty, mem_closure_iff_clusterPt, ← accPt_principal_iff_clusterPt] at h
exact h
