proposition: Corollary diff_continuous: forall (X:TopologicalSpace) (f g:point_set X -> point_set RTop) (x:point_set X), continuous_at f x -> continuous_at g x -> continuous_at (fun x:point_set X => f x - g x) x (Y:=RTop).
proof: Proof. intros. apply continuous_composition_at_2arg; trivial. apply continuous_func_continuous_everywhere. exact Rminus_continuous. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)