proposition: Lemma Rminus_continuous: continuous_2arg Rminus (X:=RTop) (Y:=RTop) (Z:=RTop).
proof: Proof. unfold Rminus. apply pointwise_continuity_2arg; intros. red. pose proof (sum_continuous _ (fun p:point_set (ProductTopology2 RTop RTop) => fst p) (fun p:point_set (ProductTopology2 RTop RTop) => -snd p) (x,y)). simpl in H. match goal with |- continuous_at ?f ?q => replace f with (fun p:R*R => fst p + - snd p) end. - apply sum_continuous. + apply continuous_func_continuous_everywhere, product2_fst_continuous. + eapply (continuous_composition_at (Y:=RTop)); apply continuous_func_continuous_everywhere. * apply Ropp_continuous. * apply product2_snd_continuous. - extensionality p. now destruct p. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)