proposition: Lemma compact_Hausdorff_impl_normal_sep: forall X:TopologicalSpace, compact X -> Hausdorff X -> normal_sep X.
proof: Proof. intros X HX_compact HX_Hausdorff. apply compact_Hausdorff_impl_T3_sep in HX_Hausdorff as [HX_T1 HX_regular]; try assumption. split; try assumption. intros F G HF_closed HG_closed HFG_disjoint. pose (P := fun y => (fun p : Ensemble X * Ensemble X => open (fst p) /\ open (snd p) /\ Intersection (fst p) (snd p) = Empty_set /\ In (fst p) y /\ Included G (snd p))). pose (cover_of_F := fun U => exists V y, In (P y) (U, V)). assert (forall U, In cover_of_F U -> open U) as Hcover_open. { intros U HU. destruct HU as [V [y []]]. intuition. } destruct (closed_compact_ens X F HX_compact HF_closed cover_of_F) as [fincover [Hfincover0 [Hfincover1 Hfincover2]]]; auto. { intros y Hy. specialize (HX_regular y G) as [U [V [HU [HV [HUx [HVx0]]]]]]; auto. { intros ?. assert (In Empty_set y); try contradiction. rewrite <- HFG_disjoint; split; assumption. } exists U; auto. exists V, y. repeat split; auto. } destruct (finite_ens_pair_choice fincover (fun U V => exists y, In (P y) (U, V))) as [fincomplement [Hfincomplement0 [Hfincomplement1 Hfincomplement2]]]; auto. exists (FamilyUnion fincover), (FamilyIntersection fincomplement). repeat split; auto using open_family_union. 1: apply open_finite_family_intersection; auto. 1,2: intros V H0; specialize (Hfincomplement2 V H0) as [? [? [? []]]]; intuition. apply Extensionality_Ensembles; split; auto with sets; red; intros. destruct H. destruct H0. destruct H as [S ? HS_fincover]. specialize (Hfincomplement1 S HS_fincover) as [U [? [y []]]]. intuition. simpl in *. specialize (H0 U H1). rewrite <- H3. split; assumption. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)