Description: This lemma is used to prove the existence of a function p as in Lemma 1 of BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 <= p <= 1, p__(t_0) = 0, and p > 0 on T - U. Here ( qi ) is used to represent p__(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | stoweidlem35.1 | |
|
stoweidlem35.2 | |
||
stoweidlem35.3 | |
||
stoweidlem35.4 | |
||
stoweidlem35.5 | |
||
stoweidlem35.6 | |
||
stoweidlem35.7 | |
||
stoweidlem35.8 | |
||
stoweidlem35.9 | |
||
stoweidlem35.10 | |
||
stoweidlem35.11 | |
||
Assertion | stoweidlem35 | |