proposition: Lemma pasting_lemma_fn_eq_inverse_image (Hfg : forall (x : X) H0 H1, f (exist _ x H0) = g (exist _ x H1)) (U : Ensemble Y) : inverse_image pasting_lemma_fn U = Union (Im (inverse_image f U) (subspace_inc _)) (Im (inverse_image g U) (subspace_inc _)).
proof: Proof. Proof using Type. apply Extensionality_Ensembles; split; red. - intros x Hx. inversion Hx; subst; clear Hx. unfold pasting_lemma_fn in H. destruct (classic_dec _). + left. exists (exist _ x i). * constructor. assumption. * reflexivity. + right. eexists (exist _ x _). * constructor. eassumption. * reflexivity. - intros x Hx. constructor. destruct Hx as [x Hx|x Hx]. + inversion Hx; subst; clear Hx. destruct H. destruct x0 as [x Hx]. simpl. erewrite pasting_lemma_fn_left; eauto. + inversion Hx; subst; clear Hx. destruct H. destruct x0 as [x Hx]. simpl. destruct (classic (In A x)). { unshelve erewrite pasting_lemma_fn_left; eauto. erewrite Hfg; eauto. } erewrite pasting_lemma_fn_right; eauto. Qed.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)