proposition: Lemma Rabs_continuous: continuous Rabs (X:=RTop) (Y:=RTop).
proof: Proof. apply pointwise_continuity. intros. apply metric_space_fun_continuity with R_metric R_metric; try apply RTop_metrization. intros. exists eps; split; trivial. intros. apply Rle_lt_trans with (2 := H0). apply Rabs_triang_inv2. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)