proposition: Lemma BishopCompact_Compact_BishopCompact2 : forall (P:Complete X->Prop) (HP:CompactSubset _ P) x, inCompact x (BishopCompactAsCompact HP) -> P x.
proof: Proof. intros P [HP1 HP2 HP3] x Hx. assert (Y:forall e:Qpos, proj1_sig ((7#8)*e)%Qpos < proj1_sig e). intros. rewrite -> Qlt_minus_iff. simpl. ring_simplify. apply (Qpos_ispos ((1#8)*e)). assert (A:forall (e:Qpos), {y | P y /\ ball (m:=Complete X) (proj1_sig e) x y}). intros e. assert (Hx':=Hx ((1#16)*e)%Qpos ((1#2)*e)%Qpos). unfold BishopCompactAsCompact, approximate, BishopCompactAsCompact_raw, totallyBoundedSubset in Hx'. clear - Hx' locatedX Y. destruct (HP2 ((1 # 2) * ((1 # 2) * e))%Qpos) as [l Hl0 Hl1]. clear Hl1. induction l. exfalso; exact (FinSubset_ball_nil Hx'). destruct (@Complete_located _ locatedX _ _ x a (Y e)) as [A|A]. exists a. split; auto. apply IHl. intros y Hy. apply Hl0; auto with *. apply FinSubset_ball_orC in Hx'. destruct Hx' as [G | Hx' | Hx'] using orC_ind. intro abs; contradict G; intro G; contradiction. elim A. clear - Hx'. rewrite <- ball_Cunit in Hx'. assert (QposEq ((7 # 8) * e) ((1#16)*e + ((1 # 16) * e + (1 # 2) * e) + (((1 # 2) * ((1 # 2) * e))))) by (unfold QposEq; simpl; ring). unfold QposEq in H. rewrite H. clear H. eapply ball_triangle. eapply ball_triangle. apply ball_approx_r. apply Hx'. apply ball_approx_l. assumption. set (f:=fun e => (let (y,_):= (A e) in y)). assert (Hf0:forall e:Qpos, ball (m:=Complete X) (proj1_sig e) (f e) x). intros e. unfold f. destruct (A e) as [y [_ Hy]]. apply ball_sym. assumption. assert (Hf: is_RegularFunction (@ball (Complete X)) (fun e => match e with QposInfinity => f (1#1)%Qpos | Qpos2QposInf e' => f e' end)). intros e1 e2. apply ball_triangle with x. apply Hf0. apply ball_sym. apply Hf0. set (f':=(Build_RegularFunction Hf)). assert (Hf1 : forall (e:Qpos), P (approximate f' e)). intros e. simpl; unfold f. destruct (A e). tauto. destruct (HP1 f') as [y Hy]. intros [e|]; apply Hf1. unfold ExtSubset in HP3. rewrite -> (HP3 x y); auto. rewrite <- Cunit_eq. rewrite -> m. intros e1 e2. apply ball_sym. rewrite Qplus_comm. apply ball_weak. rewrite Qplus_0_r. apply Qpos_nonneg. apply Hf0. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround