Carrying a basis from families of sets to families of opens

A basis of a topological space is presented in two ways in Mathlib, and neither is canonical: TopologicalSpace.IsTopologicalBasis takes a Set (Set X), while TopologicalSpace.Opens.IsBasis takes a Set (Opens X). This file bridges the first form to the second, for consumers stated in terms of Opens — the sheaf-theoretic ones, since Opens X is the category a presheaf on X is indexed by.

Main results

• TauCeti.TopologicalSpace.Opens.isBasis_of_isTopologicalBasis : a basis presented as a family of sets yields one presented as a family of Opens.

theorem TauCeti.TopologicalSpace.Opens.isBasis_of_isTopologicalBasis {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hS : TopologicalSpace.IsTopologicalBasis S) : TopologicalSpace.Opens.IsBasis {U : TopologicalSpace.Opens X | ↑U ∈ S}

A basis of sets is a basis of opens. A basis presented as a Set (Set X), the form TopologicalSpace.IsTopologicalBasis takes, yields one presented as a Set (Opens X), the form Opens.IsBasis takes: keep the opens whose underlying set is a member. Nothing is lost, since every member of a topological basis is open.

Both presentations occur in Mathlib and each has its own API, so this is a bridge between two existing forms rather than a claim that either is the standard one.