proposition: Lemma coord_continuous {K : numFieldType} m n i j : continuous (fun M : 'M[K]_(m, n) => M i j).
proof: Proof. move=> /= M s /= /(nbhs_ballP (M i j)) [e e0 es]. apply/nbhs_ballP; exists e => //= N MN; exact/es/MN. 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