proposition: Lemma Continuous_I_imp_tb_image : totally_bounded (fun_image F I).
proof: Proof. assert (H := compact_is_totally_bounded a b Hab). elim contF; intros H0 H1. split. elim H; clear H; intros H2 H3. elim H2; clear H2; intros x H. exists (Part F x (H0 _ H)). exists x; split. auto. split. apply H0; auto. algebra. intros e H2. elim (H1 _ H2). intros d H3 H4. clear H1. elim H; clear H. intros non_empty H. elim H with d; clear H. intros l Hl' Hl. 2: assumption. exists (map2 F l (fun (x : IR) (Hx : member x l) => H0 x (Hl' x Hx))). intros x H. clear Hl; induction l as [| a0 l Hrecl]. exfalso; assumption. simpl in H; elim H; clear H; intro H1. cut (forall x : IR, member x l -> compact a b Hab x). intro H. apply Hrecl with H. eapply map2_wd. apply H1. intros x0 H. apply Hl'; left; assumption. exists a0. split. apply Hl'; right; algebra. split. apply H0; apply Hl'; right; algebra. intro; eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply H1. algebra. intros x H; simpl in |- *. elim H; intros x0 H1. elim H1; clear H1; intros Hy' H1. elim H1; intros Hy'' Hy. elim (Hl x0 Hy'); intros x1 Hx1 H5. exists (F x1 (H0 x1 (Hl' x1 Hx1))). apply map2_pres_member; assumption. astepr (F x0 Hy''[-]F x1 (H0 x1 (Hl' x1 Hx1))). apply AbsIR_imp_AbsSmall. apply H4. assumption. apply Hl'; assumption. apply AbsSmall_imp_AbsIR; assumption. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac