proposition: Lemma compact_eqDom : forall X1 X2:R -> Prop, compact X1 -> X1 =_D X2 -> compact X2.
proof: Proof. unfold compact; intros; unfold eq_Dom in H0; elim H0; clear H0; unfold included; intros; assert (H3 : covering_open_set X1 f0). - unfold covering_open_set; unfold covering_open_set in H1; elim H1; clear H1; intros; split. + unfold covering in H1; unfold covering; intros; apply (H1 _ (H0 _ H4)). + apply H3. - elim (H _ H3); intros D H4; exists D; unfold covering_finite; unfold covering_finite in H4; elim H4; intros; split. + unfold covering in H5; unfold covering; intros; apply (H5 _ (H2 _ H7)). + apply H6. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type