proposition: Lemma open_basis_to_open_neighborhood_basis: forall {X:TopologicalSpace} (B:Family X) (x:point_set X), open_basis B -> open_neighborhood_basis [ U:Ensemble X | In B U /\ In U x ] x.
proof: Proof. intros. destruct H. constructor; intros. - now split; destruct H as [[? ?]]; [ apply open_basis_elements | ]. - destruct H. destruct (open_basis_cover x U H H0). destruct H1 as [? [? ?]]. exists x0. now repeat split. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases