proposition: Lemma dense_in_closure {X:TopologicalSpace} (A : Ensemble X) : dense (inverse_image (subspace_inc (closure A)) A).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. { constructor. } destruct x. rewrite subspace_closure. constructor. simpl. rewrite inverse_image_image_surjective_locally. { assumption. } intros. unshelve eexists (exist _ y _). 2: { reflexivity. } apply closure_inflationary. assumption. Qed.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)