proposition: Lemma sum_topology_open_full_set_component {A : Type} (X : forall a, TopologicalSpace) : forall a, @open (SumTopology A X) (Im Full_set (sum_space_point_set_intro X a)).
proof: Proof. intros a1 a2. destruct (classic (a1 = a2)). - subst. replace (inverse_image (sum_space_point_set_intro X a2) (Im Full_set (sum_space_point_set_intro X a2))) with (@Full_set (point_set (X a2))). + apply open_full. + extensionality_ensembles; repeat econstructor. - replace (inverse_image (sum_space_point_set_intro X a2) (Im Full_set (sum_space_point_set_intro X a1))) with (@Empty_set (point_set (X a2))). + apply open_empty. + extensionality_ensembles_inv. subst. injection H2 as H2. now subst. Qed.
imports: TopologicalSpaces StrongTopology Compactness ZornsLemma(DependentTypeChoice EnsemblesTactics)