proposition: Lemma continuous_at_is_local: forall (X Y:TopologicalSpace) (x0:X) (f g:X -> Y) (N:Ensemble X), neighborhood N x0 -> (forall x:point_set X, In N x -> f x = g x) -> continuous_at f x0 -> continuous_at g x0.
proof: Proof. intros. red; intros. destruct H as [U1 [[]]]. rewrite <- H0 in H2. 2: { auto. } apply H1 in H2. destruct H2 as [U2 [[]]]. exists (Intersection U1 U2). repeat split; trivial. - apply open_intersection2; trivial. - destruct H7. rewrite <- H0. + apply H6 in H8. destruct H8; trivial. + auto. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases NeighborhoodBases Subbases