proposition: Lemma mule_continuous (r : R) : continuous (mule r%:E).
proof: Proof. rewrite /continuous_at; wlog r0 : r / (r > 0)%R => [hwlog|]. have [r0|r0|->] := ltrgtP r 0; do ?exact: hwlog; last first. by move=> x; rewrite mul0e; apply: cvg_near_cst; near=> y; rewrite mul0e. have -> : *%E r%:E = \- ( *%E (- r)%:E ). by apply/funeqP=> x /=; rewrite EFinN mulNe oppeK. move=> x; apply: (continuous_comp (hwlog (- r)%R _ _)); rewrite ?oppr_gt0//. exact: oppe_continuous. move=> [s||]/=. - rewrite -EFinM; apply: cvg_EFin => /=. by apply/nbhs_EFin; near do rewrite fin_numM//. move=> P /= Prs; apply/nbhs_EFin=> //=. by apply: near_fun => //=; apply: continuousM => //=; apply: cvg_cst. - rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]]. exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW. by move=> x rux; apply: uA; move: rux; rewrite EFinM lte_pdivr_mull. - rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]]. exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW. by move=> x xru; apply: uA; move: xru; rewrite EFinM lte_pdivl_mull. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule