Mathlib Map

Theorems · Definition · general topology

Perfect.casesOn

{α : Type u_1} →
  [inst : TopologicalSpace α] →
    {C : Set α} →
      {motive : Perfect C → Sort u} →
        (t : Perfect C) → ((closed : IsClosed C) → (acc : Preperfect C) → motive ⋯) → motive t
Defined in
Mathlib.Topology.Perfect
Cited by
1 results in Mathlib
Foundations
Depth 53 from the axioms · uses propext, Quot.sound
Assumes
TopologicalSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

perfect_def · cited by 1perfect_defSet · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpaceIsClosed · cited by 1639IsClosedPreperfect · cited by 19PreperfectPerfect · cited by 17PerfectPerfect.casesOnCITED BYCITES

Cites5

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
  • IsClosedstatement and proof · cited by 1,639
  • Preperfectstatement and proof · cited by 19
  • Perfectstatement and proof · cited by 17

Cited by1

Results whose statement or proof uses this declaration.