proposition: Lemma compact_P4 : forall X F:R -> Prop, compact X -> closed_set F -> included F X -> compact F.
proof: Proof. unfold compact; intros; elim (classic (exists z : R, F z)); intro Hyp_F_NE. - set (D := ind f0); set (g := f f0); unfold closed_set in H0. set (g' := fun x y:R => f0 x y \/ complementary F y /\ D x). set (D' := D). cut (forall x:R, (exists y : R, g' x y) -> D' x). 1:intro; set (f' := mkfamily D' g' H3); cut (covering_open_set X f'). + intro; elim (H _ H4); intros DX H5; exists DX. unfold covering_finite; unfold covering_finite in H5; elim H5; clear H5; intros. split. * unfold covering; unfold covering in H5; intros. elim (H5 _ (H1 _ H7)); intros y0 H8; exists y0; simpl in H8; simpl; elim H8; clear H8; intros. split. -- unfold g' in H8; elim H8; intro. ++ apply H10. ++ elim H10; intros H11 _; unfold complementary in H11; elim H11; apply H7. -- apply H9. * unfold family_finite; unfold domain_finite; unfold family_finite in H6; unfold domain_finite in H6; elim H6; clear H6; intros l H6; exists l; intro; assert (H7 := H6 x); elim H7; clear H7; intros. split. -- intro; apply H7; simpl; unfold intersection_domain; simpl in H9; unfold intersection_domain in H9; unfold D'; apply H9. -- intro; assert (H10 := H8 H9); simpl in H10; unfold intersection_domain in H10; simpl; unfold intersection_domain; unfold D' in H10; apply H10. + unfold covering_open_set; unfold covering_open_set in H2; elim H2; clear H2; intros. split. * unfold covering; unfold covering in H2; intros. elim (classic (F x)); intro. -- elim (H2 _ H6); intros y0 H7; exists y0; simpl; unfold g'; left; assumption. -- cut (exists z : R, D z). ++ intro; elim H7; clear H7; intros x0 H7; exists x0; simpl; unfold g'; right. split. ** unfold complementary; apply H6. ** apply H7. ++ elim Hyp_F_NE; intros z0 H7. assert (H8 := H2 _ H7). elim H8; clear H8; intros t H8; exists t; apply (cond_fam f0); exists z0; apply H8. * unfold family_open_set; intro; simpl; unfold g'; elim (classic (D x)); intro. -- apply open_set_P6 with (union_domain (f0 x) (complementary F)). ++ apply open_set_P2. ** unfold family_open_set in H4; apply H4. ** apply H0. ++ unfold eq_Dom; split. ** unfold included, union_domain, complementary; intros. elim H6; intro; [ left; apply H7 | right; split; assumption ]. ** unfold included, union_domain, complementary; intros. elim H6; intro; [ left; apply H7 | right; elim H7; intros; apply H8 ]. -- apply open_set_P6 with (f0 x). ++ unfold family_open_set in H4; apply H4. ++ unfold eq_Dom; split. ** unfold included, complementary; intros; left; apply H6. ** unfold included, complementary; intros. elim H6; intro. { apply H7. } elim H7; intros _ H8; elim H5; apply H8. + intros; elim H3; intros y0 H4; unfold g' in H4; elim H4; intro. * apply (cond_fam f0); exists y0; apply H5. * elim H5; clear H5; intros _ H5; apply H5. - cut (compact F). + intro; apply (H3 f0 H2). + apply compact_eqDom with (fun _:R => False). * apply compact_EMP. * unfold eq_Dom; split. -- unfold included; intros; elim H3. -- assert (H3 := not_ex_all_not _ _ Hyp_F_NE); unfold included; intros; elim (H3 x); apply H4. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type