proposition: Lemma subspace_closure U : closure U = inverse_image subspace_inc (closure (Im U subspace_inc)).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - constructor. apply continuous_closure. { apply subspace_inc_continuous. } apply Im_def. assumption. - destruct H. unfold closure in H. constructor. intros. destruct H0. destruct H0. rewrite subspace_closed_char in H0. destruct H0 as [V []]. subst. constructor. destruct H. apply H. repeat split; try assumption. intros ? ?. inversion H2; subst; clear H2. apply H1. assumption. Qed.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)