Description: This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91: assuming that R is a finite subset of V , x indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ x_i ≤ 1, x_i < ε / m on V(t_i), and x_i > 1 - ε / m on B . Here M is used to represent m in the paper, E is used to represent ε in the paper, v_i is used to represent V(t_i). (Contributed by Glauco Siliprandi, 20-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | stoweidlem31.1 | |
|
stoweidlem31.2 | |
||
stoweidlem31.3 | |
||
stoweidlem31.4 | |
||
stoweidlem31.5 | |
||
stoweidlem31.6 | |
||
stoweidlem31.7 | |
||
stoweidlem31.8 | |
||
stoweidlem31.9 | |
||
stoweidlem31.10 | |
||
stoweidlem31.11 | |
||
stoweidlem31.12 | |
||
stoweidlem31.13 | |
||
stoweidlem31.14 | |
||
Assertion | stoweidlem31 | |