proposition: Lemma continuity_compact : forall (f:R -> R) (X:R -> Prop), (forall x:R, continuity_pt f x) -> compact X -> compact (image_dir f X).
proof: Proof. unfold compact; intros; unfold covering_open_set in H1. elim H1; clear H1; intros. set (D := ind f1). set (g := fun x y:R => image_rec f0 (f1 x) y). cut (forall x:R, (exists y : R, g x y) -> D x). 1:intro; set (f' := mkfamily D g H3). 1:cut (covering_open_set X f'). - intro; elim (H0 f' H4); intros D' H5; exists D'. unfold covering_finite in H5; elim H5; clear H5; intros; unfold covering_finite; split. + unfold covering, image_dir; simpl; unfold covering in H5; intros; elim H7; intros y H8; elim H8; intros; assert (H11 := H5 _ H10); simpl in H11; elim H11; intros z H12; exists z; unfold g in H12; unfold image_rec in H12; rewrite H9; apply H12. + unfold family_finite in H6; unfold domain_finite in H6; unfold family_finite; unfold domain_finite; elim H6; intros l H7; exists l; intro; elim (H7 x); intros; split; intro. * apply H8; simpl in H10; simpl; apply H10. * apply (H9 H10). - unfold covering_open_set; split. + unfold covering; intros; simpl; unfold covering in H1; unfold image_dir in H1; unfold g; unfold image_rec; apply H1. exists x; split; [ reflexivity | apply H4 ]. + unfold family_open_set; unfold family_open_set in H2; intro; simpl; unfold g; cut ((fun y:R => image_rec f0 (f1 x) y) = image_rec f0 (f1 x)). * intro; rewrite H4. apply (continuity_P2 f0 (f1 x) H (H2 x)). * reflexivity. - intros; apply (cond_fam f1); unfold g in H3; unfold image_rec in H3; elim H3; intros; exists (f0 x0); apply H4. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type