proposition: Lemma compact_EMP : compact (fun _:R => False).
proof: Proof. unfold compact; intros; exists (fun x:R => False); unfold covering_finite; split. - unfold covering; intros; elim H0. - unfold family_finite; unfold domain_finite; exists nil; intro. split. + simpl; unfold intersection_domain; intros; elim H0. elim H0; clear H0; intros _ H0; elim H0. + simpl; intro; elim H0. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type