structure PiBase.Development (X : Type u) [TopologicalSpace X] : Type (u + 1)

• idx : ℕ → Type u
• toCover {n : ℕ} : self.idx n → Set X
• isOpen (n : ℕ) (t : self.idx n) : IsOpen (self.toCover t)
• isCover (n : ℕ) : ⋃ (t : self.idx n), self.toCover t = Set.univ
• isLocalBase (x : X) : (nhds x).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => CoverStar self.toCover x

class PiBase.DevelopableSpace (X : Type u) [TopologicalSpace X] : Prop

• developable : Nonempty (Development X)