fact: Definition pasting_lemma_fn (x : X) : Y := match classic_dec (In A x) with | left Hx => f (exist A x Hx) | right HA => g (exist B x (Union_Full_set x HA)) end.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)