proposition: Lemma sum_topology_inj_image_open {A : Type} (X : forall a, TopologicalSpace) (a : A) (S : Ensemble (point_set (X a))) : open S <-> @open (SumTopology A X) (Im S (sum_space_point_set_intro X a)).
proof: Proof. split; intros. - intro a'. destruct (classic (a = a')). + subst. replace (inverse_image (sum_space_point_set_intro X a') (Im S (sum_space_point_set_intro X a'))) with S; trivial. extensionality_ensembles_inv. * now repeat econstructor. * injection H2 as H2. apply inj_pair2 in H2. now subst. + replace (inverse_image (sum_space_point_set_intro X a') (Im S (sum_space_point_set_intro X a))) with (@Empty_set (point_set (X a'))). * apply open_empty. * extensionality_ensembles_inv. injection H3 as H3. now subst. - replace S with (inverse_image (sum_space_point_set_intro X a) (Im S (sum_space_point_set_intro X a))). + apply H. + extensionality_ensembles_inv. * injection H2 as H2. apply inj_pair2 in H2. now subst. * now repeat econstructor. Qed.
imports: TopologicalSpaces StrongTopology Compactness ZornsLemma(DependentTypeChoice EnsemblesTactics)