Description: Lemma for cvmlift . Induction step for cvmliftlem7 . Assuming that Q ( M - 1 ) is defined at ( M - 1 ) / N and is a preimage of G ( ( M - 1 ) / N ) , the next segment Q ( M ) is also defined and is a function on W which is a lift G for this segment. This follows explicitly from the definition Q ( M ) =`' ( F |`I ) o. G since G is in 1st( FM ) for the entire interval so that ` ``' ( F |`I ) maps this into I and F o. Q maps back to G . (Contributed by Mario Carneiro, 16-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cvmliftlem.1 | |
|
cvmliftlem.b | |
||
cvmliftlem.x | |
||
cvmliftlem.f | |
||
cvmliftlem.g | |
||
cvmliftlem.p | |
||
cvmliftlem.e | |
||
cvmliftlem.n | |
||
cvmliftlem.t | |
||
cvmliftlem.a | |
||
cvmliftlem.l | |
||
cvmliftlem.q | |
||
cvmliftlem5.3 | |
||
cvmliftlem6.1 | |
||
cvmliftlem6.2 | |
||
Assertion | cvmliftlem6 | |