Theorems · Theorem · general topology

exists_perfect_nonempty_of_isClosed_of_not_countable

∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} [SecondCountableTopology α],
  IsClosed C → ¬C.Countable → ∃ D, Perfect D ∧ D.Nonempty ∧ D ⊆ C

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

Defined in: Mathlib.Topology.Perfect
Cited by: 1 results in Mathlib
Foundations: Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace SecondCountableTopology

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
Set.Nonemptystatement · cited by 2,627
IsClosedstatement and proof · cited by 1,639
SecondCountableTopologystatement and proof · cited by 750
Set.Countablestatement and proof · cited by 545
Set.subset_union_rightproof · cited by 123
Set.nonempty_iff_ne_emptyproof · cited by 96
Set.union_emptyproof · cited by 78
Perfectstatement and proof · cited by 17
exists_countable_union_perfect_of_isClosedproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

IsClosed.exists_nat_bool_injection_of_not_countableproof · cited by 0