proposition: Lemma abse_continuous : continuous (@abse R).
proof: Proof. case=> [r|A /= [r [rreal rA]]|A /= [r [rreal rA]]]/=. - exact/(cvg_comp (@norm_continuous _ [the normedModType R of R^o] r)). - by exists r; split => // y ry; apply: rA; rewrite (lt_le_trans ry)// lee_abs. - exists (- r)%R; rewrite realN; split => // y; rewrite EFinN -lteNr => yr. by apply: rA; rewrite (lt_le_trans yr)// -abseN lee_abs. 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