proposition: Lemma continuous_func_continuous_everywhere: continuous -> forall x:point_set X, continuous_at x.
proof: Proof. intros. apply continuous_at_open_neighborhoods. intros. apply open_neighborhood_is_neighborhood. destruct H0; split; try constructor; auto. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases NeighborhoodBases Subbases