proposition: Lemma compact_Hausdorff_impl_T3_sep: forall X:TopologicalSpace, compact X -> Hausdorff X -> T3_sep X.
proof: Proof. intros X HX_compact HX_Hausdorff. split. { now apply Hausdorff_impl_T1_sep. } intros x F HF HFx. 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) x /\ In (snd p) y)). pose (cover_of_F := fun V => exists U y, In (P y) (U, V)). assert (forall V, In cover_of_F V -> open V) as Hcover_open. { intros V HV. destruct HV as [U [y []]]. intuition. } destruct (closed_compact_ens X F HX_compact HF cover_of_F) as [fincover [Hfincover0 [Hfincover1 Hfincover2]]]; auto. { intros y Hy. specialize (HX_Hausdorff x y) as [U [V [HU [HV [HUx [HVx0]]]]]]. { intros ?. subst. contradiction. } exists V; auto. exists U, y. repeat split; auto. } destruct (finite_ens_pair_choice fincover (fun V U => exists y, In (P y) (U, V))) as [fincomplement [Hfincomplement0 [Hfincomplement1 Hfincomplement2]]]; auto. exists (FamilyIntersection fincomplement), (FamilyUnion fincover). 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 H. destruct H0 as [S ? HS_fincover]. specialize (Hfincomplement1 S HS_fincover) as [U [? [y []]]]. intuition. simpl in *. specialize (H U H1). rewrite <- H3. split; assumption. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)