exists_perfect_nonempty_of_isClosed_of_not_countable

English

Any uncountable closed set in a second-countable space contains a nonempty perfect subset.

Русский

Любое несчётное замкнутое множество во втором счётном пространстве содержит непустое совершенное подмножество.

LaTeX

$$$\exists D \; (\text{Perfect } D) \land D \neq \emptyset \land D \subseteq C.$$$

Lean4

/-- Any uncountable closed set in a second countable space contains a nonempty perfect subset. -/
theorem exists_perfect_nonempty_of_isClosed_of_not_countable [SecondCountableTopology α] (hclosed : IsClosed C)
    (hunc : ¬C.Countable) : ∃ D : Set α, Perfect D ∧ D.Nonempty ∧ D ⊆ C :=
  by
  rcases exists_countable_union_perfect_of_isClosed hclosed with ⟨V, D, Vct, Dperf, VD⟩
  refine ⟨D, ⟨Dperf, ?_⟩⟩
  constructor
  · rw [nonempty_iff_ne_empty]
    by_contra h
    rw [h, union_empty] at VD
    rw [VD] at hunc
    contradiction
  rw [VD]
  exact subset_union_right

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