proposition: Lemma scale_continuous : continuous (fun z : K * V => z.1 *: z.2).
proof: Proof. move=> [/= k x]; apply/cvgrPdist_lt => _/posnumP[e]; near +oo_K => M. near=> l z => /=; have M0 : 0 < M by []. rewrite (@distm_lt_split _ _ (k *: z)) // -?(scalerBr, scalerBl) normrZ. rewrite (@le_lt_trans _ _ (M * `|x - z|)) ?ler_wpM2r -?ltr_pdivlMl//. by near: z; apply: cvgr_dist_lt; rewrite // mulr_gt0 ?invr_gt0. rewrite (@le_lt_trans _ _ (`|k - l| * M)) ?ler_wpM2l -?ltr_pdivlMr//. by near: z; near: M; apply: cvg_bounded (@cvg_refl _ _). by near: l; apply: cvgr_dist_lt; rewrite // divr_gt0. 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