proposition: Lemma continuous_funext {X Y : TopologicalSpace} (f g : X -> Y) : (forall x, f x = g x) -> continuous f -> continuous g.
proof: Proof. intros Hfg Hf U HU. replace (inverse_image g U) with (inverse_image f U); auto. extensionality_ensembles; constructor; rewrite Hfg in *; assumption. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases NeighborhoodBases Subbases