proposition: Lemma locally_compactR (R : realType) : locally_compact [set: R].
proof: Proof. move=> x _; rewrite withinET; exists (closed_ball x 1). by apply/nbhs_closedballP; exists 1%:pos. by split; [apply: closed_ballR_compact | apply: closed_ball_closed]. 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