proposition: Lemma Rplus_continuous: continuous_2arg Rplus (X:=RTop) (Y:=RTop) (Z:=RTop).
proof: Proof. apply pointwise_continuity_2arg. intros. red. pose proof (RTop_metrization (x+y)). apply continuous_at_neighborhood_basis with (metric_topology_neighborhood_basis R_metric (x+y)). - apply open_neighborhood_basis_is_neighborhood_basis, RTop_metrization. - intros. destruct H0. exists (EnsembleProduct (open_ball R_metric x (r/2)) (open_ball R_metric y (r/2))). repeat split; try (rewrite metric_zero; apply R_metric_is_metric + lra). + apply ProductTopology2_basis_is_basis. constructor; apply metric_space_open_ball_open; auto using RTop_metrization, R_metric_is_metric. + destruct x0 as [x' y'], H1 as [[] []]. unfold R_metric. simpl. replace (x'+y' - (x+y)) with ((x'-x) + (y'-y)) by ring. apply Rle_lt_trans with (Rabs (x'-x) + Rabs(y'-y)). * apply Rabs_triang. * replace r with (r/2+r/2) by field. now apply Rplus_lt_compat. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)