proposition: Lemma compact_P6 : forall X:R -> Prop, compact X -> (exists z : R, X z) -> forall g:family, family_closed_set g -> intersection_vide_in X g -> exists D : R -> Prop, intersection_vide_finite_in X (subfamily g D).
proof: Proof. intros X H Hyp g H0 H1. set (D' := ind g). set (f' := fun x y:R => complementary (g x) y /\ D' x). assert (H2 : forall x:R, (exists y : R, f' x y) -> D' x). { intros; elim H2; intros; unfold f' in H3; elim H3; intros; assumption. } set (f0 := mkfamily D' f' H2). unfold compact in H; assert (H3 : covering_open_set X f0). - unfold covering_open_set; split. + unfold covering; intros; unfold intersection_vide_in in H1; elim (H1 x); intros; unfold intersection_family in H5; assert (H6 := not_ex_all_not _ (fun y:R => forall y0:R, ind g y0 -> g y0 y) H5 x); assert (H7 := not_all_ex_not _ (fun y0:R => ind g y0 -> g y0 x) H6); elim H7; intros; exists x0; elim (imply_to_and _ _ H8); intros; unfold f0; simpl; unfold f'; split; [ apply H10 | apply H9 ]. + unfold family_open_set; intro; elim (classic (D' x)); intro. * apply open_set_P6 with (complementary (g x)). -- unfold family_closed_set in H0; unfold closed_set in H0; apply H0. -- unfold f0; simpl; unfold f'; unfold eq_Dom; split. ++ unfold included; intros; split; [ apply H4 | apply H3 ]. ++ unfold included; intros; elim H4; intros; assumption. * apply open_set_P6 with (fun _:R => False). -- apply open_set_P4. -- unfold eq_Dom; unfold included; split; intros; [ elim H4 | simpl in H4; unfold f' in H4; elim H4; intros; elim H3; assumption ]. - elim (H _ H3); intros SF H4; exists SF; unfold intersection_vide_finite_in; split. + unfold intersection_vide_in; simpl; intros; split. * intros; unfold included; intros; unfold intersection_vide_in in H1; elim (H1 x); intros; elim H6; intros; apply H7. -- unfold intersection_domain in H5; elim H5; intros; assumption. -- assumption. * elim (classic (exists y : R, intersection_domain (ind g) SF y)); intro Hyp'. -- red; intro; elim H5; intros; unfold intersection_family in H6; simpl in H6. cut (X x0). ++ intro; unfold covering_finite in H4; elim H4; clear H4; intros H4 _; unfold covering in H4; elim (H4 x0 H7); intros; simpl in H8; unfold intersection_domain in H6; cut (ind g x1 /\ SF x1). ** intro; assert (H10 := H6 x1 H9); elim H10; clear H10; intros H10 _; elim H8; clear H8; intros H8 _; unfold f' in H8; unfold complementary in H8; elim H8; clear H8; intros H8 _; elim H8; assumption. ** split. { apply (cond_fam f0). exists x0; elim H8; intros; assumption. } elim H8; intros; assumption. ++ unfold intersection_vide_in in H1; elim Hyp'; intros; assert (H8 := H6 _ H7); elim H8; intros; cut (ind g x1). ** intro; elim (H1 x1); intros; apply H12. { apply H11. } apply H9. ** apply (cond_fam g); exists x0; assumption. -- unfold covering_finite in H4; elim H4; clear H4; intros H4 _; cut (exists z : R, X z). ++ intro; elim H5; clear H5; intros; unfold covering in H4; elim (H4 x0 H5); intros; simpl in H6; elim Hyp'; exists x1; elim H6; intros; unfold intersection_domain; split. ** apply (cond_fam f0); exists x0; apply H7. ** apply H8. ++ apply Hyp. + unfold covering_finite in H4; elim H4; clear H4; intros; unfold family_finite in H5; unfold domain_finite in H5; unfold family_finite; unfold domain_finite; elim H5; clear H5; intros l H5; exists l; intro; elim (H5 x); intros; split; intro; [ apply H6; simpl; simpl in H8; apply H8 | apply (H7 H8) ]. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type