proposition: Lemma compact_image_ens {X Y : TopologicalSpace} (f : X -> Y) (U : Ensemble X) : continuous f -> compact (SubspaceTopology U) -> compact (SubspaceTopology (Im U f)).
proof: Proof. intros. unshelve eapply (@compact_image (SubspaceTopology U)). { refine (fun p => exist _ (f (proj1_sig p)) _). apply Im_def. apply proj2_sig. } 1: assumption. { apply subspace_continuous_char. unfold compose. simpl. apply (continuous_composition f). - assumption. - apply subspace_inc_continuous. } intros [y Hy]. inversion Hy; subst. exists (exist _ x H1). simpl. apply subset_eq. reflexivity. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)