proposition: Lemma bounded_closed_compact (R : realType) n (A : set 'rV[R]_n.+1) : bounded_set A -> closed A -> compact A.
proof: Proof. move=> [M [Mreal normAltM]] Acl. have Mnco : compact [set v : 'rV[R]_n.+1 | forall i, v ord0 i \in `[(- (M + 1)), (M + 1)]]. apply: (@rV_compact _ _ (fun _ => `[(- (M + 1)), (M + 1)]%classic)). by move=> _; apply: segment_compact. apply: subclosed_compact Acl Mnco _ => v /normAltM normvleM i. suff : `|v ord0 i : R| <= M + 1 by rewrite ler_norml. apply: le_trans (normvleM _ _); last by rewrite ltrDl. have /mapP[j Hj ->] : `|v ord0 i| \in [seq `|v x.1 x.2| | x : 'I_1 * 'I_n.+1]. by apply/mapP; exists (ord0, i) => //=; rewrite mem_enum. by rewrite [leRHS]/normr /= mx_normrE; apply/bigmax_geP; right => /=; exists j. 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