Description: This lemma proves that there exists a function x as in the proof in BrosowskiDeutsh p. 91, after Lemma 2: x_j is in the subalgebra, 0 <= x_j <= 1, x_j < ε / n on A_j (meaning A in the paper), x_j > 1 - \epsilon / n on B_j. Here D is used to represent A in the paper (because A is used for the subalgebra of functions), E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | stoweidlem59.1 | |
|
stoweidlem59.2 | |
||
stoweidlem59.3 | |
||
stoweidlem59.4 | |
||
stoweidlem59.5 | |
||
stoweidlem59.6 | |
||
stoweidlem59.7 | |
||
stoweidlem59.8 | |
||
stoweidlem59.9 | |
||
stoweidlem59.10 | |
||
stoweidlem59.11 | |
||
stoweidlem59.12 | |
||
stoweidlem59.13 | |
||
stoweidlem59.14 | |
||
stoweidlem59.15 | |
||
stoweidlem59.16 | |
||
stoweidlem59.17 | |
||
stoweidlem59.18 | |
||
stoweidlem59.19 | |
||
Assertion | stoweidlem59 | |