fact: Record neighborhood_basis {X:TopologicalSpace} (NB:Family X) (x:point_set X) : Prop := { neighborhood_basis_elements: forall N:Ensemble X, In NB N -> neighborhood N x; neighborhood_basis_cond: forall N:Ensemble X, neighborhood N x -> exists N':Ensemble X, In NB N' /\ Included N' N }.
imports: TopologicalSpaces Neighborhoods OpenBases