proposition: Lemma pointwise_continuity : (forall x:point_set X, continuous_at x) -> continuous.
proof: Proof. intros. red; intros. replace (inverse_image f V) with (interior (inverse_image f V)). { apply interior_open. } apply Extensionality_Ensembles; split. { apply interior_deflationary. } red; intros. destruct H1. assert (neighborhood V (f x)). { exists V; repeat split; auto with sets. } pose proof (H x V H2). destruct H3 as [U]. destruct H3. destruct H3. assert (Included U (interior (inverse_image f V))). { apply interior_maximal; trivial. } auto. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases NeighborhoodBases Subbases