proposition: Lemma Ropp_continuous: continuous Ropp (X:=RTop) (Y:=RTop).
proof: Proof. apply pointwise_continuity. intro. apply metric_space_fun_continuity with R_metric R_metric; try apply RTop_metrization. intros. exists eps. split; trivial. intros. unfold R_metric. replace (-x' - -x) with (x-x') by ring. now rewrite Rabs_minus_sym. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals