proposition: Lemma compact_bounded (K : realType) (V : normedModType K) (A : set V) : compact A -> bounded_set A.
proof: Proof. rewrite compact_cover => Aco. have covA : A `<=` \bigcup_(n : int) [set p | `|p| < n%:~R]. by move=> p _; exists (floor `|p| + 1) => //; rewrite rmorphD/= lt_succ_floor. have /Aco [] := covA. move=> n _; rewrite openE => p; rewrite /= -subr_gt0 => ltpn. apply/nbhs_ballP; exists (n%:~R - `|p|) => // q. rewrite -ball_normE /= ltrBrDr distrC; apply: le_lt_trans. by rewrite -{1}(subrK p q) ler_normD. move=> D _ DcovA. exists (\big[maxr/0]_(i : D) (fsval i)%:~R). rewrite bigmax_real//; last by move=> ? _; rewrite realz. split => // x ltmaxx p /DcovA [n Dn /lt_trans /(_ _)/ltW]. apply; apply: le_lt_trans ltmaxx. have : n \in enum_fset D by []. by rewrite enum_fsetE => /mapP[/= i iD ->]; exact/le_bigmax. 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