proposition: Lemma open_neighborhood_bases_to_open_basis: forall {X:TopologicalSpace} (NB : point_set X -> Family X), (forall x:point_set X, open_neighborhood_basis (NB x) x) -> open_basis (IndexedUnion NB).
proof: Proof. intros. constructor; intros. - destruct H0. destruct (H a). now destruct (open_neighborhood_basis_elements0 x H0). - destruct (H x). assert (open_neighborhood U x) by now constructor. destruct (open_neighborhood_basis_cond0 U H2) as [V [? ?]]. exists V. repeat split; trivial. + now exists x. + now destruct (open_neighborhood_basis_elements0 V H3). Qed.
imports: TopologicalSpaces Neighborhoods OpenBases