proposition: Lemma pasting_lemma_fn_left (x : X) (Hx : In A x) : pasting_lemma_fn x = f (exist A x Hx).
proof: Proof. Proof using Type. unfold pasting_lemma_fn. destruct (classic_dec _); try contradiction. destruct (proof_irrelevance _ Hx i); reflexivity. Qed.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)