proposition: Lemma sum_topology_closed_full_set_component {A : Type} (X : forall a, TopologicalSpace) : forall a, @closed (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) (@Complement (point_set (SumTopology A X)) (Im Full_set (sum_space_point_set_intro X a2)))) with (@Empty_set (point_set (X a2))). + apply open_empty. + extensionality_ensembles_inv. destruct H0. repeat econstructor. - replace (inverse_image (sum_space_point_set_intro X a2) (@Complement (point_set (SumTopology A X)) (Im Full_set (sum_space_point_set_intro X a1)))) with (@Full_set (point_set (X a2))). + apply open_full. + extensionality_ensembles_inv; repeat econstructor. intro. inversion H0. injection H3 as H3. now subst. Qed.
imports: TopologicalSpaces StrongTopology Compactness ZornsLemma(DependentTypeChoice EnsemblesTactics)