proposition: Lemma Rmult_continuous_at_origin: continuous_at_2arg Rmult 0 0 (X:=RTop) (Y:=RTop) (Z:=RTop).
proof: Proof. red. pose proof (RTop_metrization 0). apply continuous_at_neighborhood_basis with (metric_topology_neighborhood_basis R_metric 0). - apply open_neighborhood_basis_is_neighborhood_basis. simpl. rewrite Rmult_0_r. assumption. - intros. destruct H0. exists (EnsembleProduct (open_ball R_metric 0 r) (open_ball R_metric 0 1)). 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 x as [x y], H1 as [[] []]. unfold R_metric in *. simpl. rewrite Rminus_0_r in *. rewrite Rabs_mult. replace r with (r*1) by auto with real. apply Rmult_le_0_lt_compat; apply Rabs_pos + trivial. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)