proposition: Lemma topological_property_T3_sep : topological_property T3_sep.
proof: Proof. intros X Y f Hf [HT1 H]. split. - eapply topological_property_T1_sep. + exact Hf. + assumption. - destruct Hf as [g Hcont_f Hcont_g Hgf Hfg]. intros y F Hcl Hn. destruct (H (g y) (inverse_image f F)) as [U [V [HopenU [HopenV [HinU [Hincl eq]]]]]]. + red. rewrite <- inverse_image_complement. now apply Hcont_f. + intros [contra]. now rewrite Hfg in contra. + exists (inverse_image g U), (inverse_image g V). repeat split; try apply Hcont_g; trivial. * apply Hincl. constructor. now rewrite Hfg. * erewrite <- inverse_image_intersection, <- inverse_image_empty. now f_equal. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)