Theorems · Definition · general topology
Preperfect
{α : Type u_1} → [TopologicalSpace α] → Set α → PropA set C is preperfect if all of its points are accumulation points of itself.
If α is a T1 space, this is equivalent to the closure of C being perfect,
see preperfect_iff_perfect_closure. This property is also called dense-in-itself.
- Defined in
- Mathlib.Topology.Perfect
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 50 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Filter.principalproof · cited by 740
- AccPtproof · cited by 75
Cited by23
Results whose statement or proof uses this declaration.
- Perfect.accstatement · cited by 6
- PerfectSpace.univ_preperfectstatement · cited by 4
- MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin_preperfectstatement and proof · cited by 3
- Preperfect.perfect_closurestatement and proof · cited by 3
- Preperfect.open_interstatement and proof · cited by 2
- IsPreconnected.preperfect_of_nontrivialstatement · cited by 2
- preperfect_iff_nhdsstatement · cited by 2
- Complex.ECanonicalDecomp.eq_smul_meromorphicTrailingCoeffAtproof · cited by 1
- preperfect_iff_eq_relDerivedSetstatement · cited by 1
- preperfect_iff_subset_derivedSetstatement · cited by 1
- perfect_defstatement and proof · cited by 1
- perfect_iff_eq_derivedSetproof · cited by 1