proposition: Lemma continuous_constant: forall (X Y:TopologicalSpace) (y0:Y), continuous (fun x:X => y0).
proof: Proof. intros. pose (f := fun _:X => y0). fold f. red; intros. destruct (classic (In V y0)). - replace (inverse_image f V) with (@Full_set X). { apply open_full. } apply Extensionality_Ensembles; split; red; intros. + constructor; trivial. + constructor. - replace (inverse_image f V) with (@Empty_set X). { apply open_empty. } apply Extensionality_Ensembles; split; auto with sets; red; intros. destruct H1. contradiction H0. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases NeighborhoodBases Subbases