proposition: Lemma T3_sep_Subspace {X : TopologicalSpace} (A : Ensemble X) : T3_sep X -> T3_sep (SubspaceTopology A).
proof: Proof. intros [HX0 HX1]. split. { apply T1_sep_Subspace. assumption. } intros [x Hx] F HF HFx. apply subspace_closed_char in HF as [G [HG HG0]]. subst. assert (~ In G x) as HGx. { intros HGx. apply HFx. constructor. simpl. assumption. } clear HFx. specialize (HX1 x G HG HGx) as [U [V [HU [HV [HUx [HVG HUV]]]]]]. exists (inverse_image (subspace_inc A) U), (inverse_image (subspace_inc A) V). repeat split. - apply subspace_inc_continuous; assumption. - apply subspace_inc_continuous; assumption. - simpl. assumption. - apply HVG. destruct H. assumption. - rewrite <- inverse_image_intersection. rewrite HUV. apply inverse_image_empty. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)