Description: Lemma for cvmlift . Discharge the assumptions of cvmliftlem14 . The set of all open subsets u of the unit interval such that G " u is contained in an even covering of some open set in J is a cover of II by the definition of a covering map, so by the Lebesgue number lemma lebnumii , there is a subdivision of the closed unit interval into N equal parts such that each part is entirely contained within one such open set of J . Then using finite choice ac6sfi to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 . (Contributed by Mario Carneiro, 14-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cvmliftlem.1 | |
|
cvmliftlem.b | |
||
cvmliftlem.x | |
||
cvmliftlem.f | |
||
cvmliftlem.g | |
||
cvmliftlem.p | |
||
cvmliftlem.e | |
||
Assertion | cvmliftlem15 | |