Description: Lemma for lebnum . The function F measures the sum of all of the distances to escape the sets of the cover. Since by assumption it is a cover, there is at least one set which covers a given point, and since it is open, the point is a positive distance from the edge of the set. Thus, the sum is a strictly positive number. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by AV, 30-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lebnum.j | |
|
lebnum.d | |
||
lebnum.c | |
||
lebnum.s | |
||
lebnum.u | |
||
lebnumlem1.u | |
||
lebnumlem1.n | |
||
lebnumlem1.f | |
||
Assertion | lebnumlem1 | |