proposition: Lemma pasting_lemma_cts : (forall x : X, forall H0 H1, f (exist _ x H0) = g (exist _ x H1)) -> closed A -> closed B -> continuous f -> continuous g -> continuous pasting_lemma_fn.
proof: Proof. Proof using Type. intros Hfg HA HB Hf Hg. apply continuous_closed. intros U HU. rewrite pasting_lemma_fn_eq_inverse_image; auto. apply closed_union2. - apply subspace_inc_takes_closed_to_closed. + assumption. + apply continuous_closed; assumption. - apply subspace_inc_takes_closed_to_closed. + assumption. + apply continuous_closed; assumption. Qed.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)