Theorems · Inductive type · general topology
Perfect
{α : Type u_1} → [TopologicalSpace α] → Set α → PropA set C is called perfect if it is closed and all of its
points are accumulation points of itself.
Note that we do not require C to be nonempty.
- Defined in
- Mathlib.Topology.Perfect
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement · cited by 24,529
Cited by19
Results whose statement or proof uses this declaration.
- Perfect.accstatement and proof · cited by 6
- Preperfect.perfect_closurestatement · cited by 3
- IsOpen.perfect_closurestatement · cited by 2
- Perfect.closedstatement and proof · cited by 2
- Perfect.exists_nat_bool_injectionstatement and proof · cited by 2
- Perfect.small_diam_splittingstatement and proof · cited by 1
- Perfect.splittingstatement and proof · cited by 1
- Perfect.subset_perfectKernelstatement and proof · cited by 1
- exists_countable_union_perfect_of_isClosedstatement · cited by 1
- CantorBendixson.perfect_perfectKernelstatement and proof · cited by 1
- perfect_defstatement and proof · cited by 1
- perfect_iff_eq_derivedSetstatement · cited by 1