proposition: Lemma compact_carac : forall X:R -> Prop, compact X <-> closed_set X /\ bounded X.
proof: Proof. intro; split. - intro; split; [ apply (compact_P2 _ H) | apply (compact_P1 _ H) ]. - intro; elim H; clear H; intros; apply (compact_P5 _ H H0). Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type