Description: This lemma is used to prove the existence of a function p_t as in the beginning of Lemma 1 BrosowskiDeutsh p. 90: for all t in T - U, there exists a function p in the subalgebra, such that p_t ( t_0 ) = 0 , p_t ( t ) > 0, and 0 <= p_t <= 1. (Contributed by Glauco Siliprandi, 20-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | stoweidlem23.1 | |
|
stoweidlem23.2 | |
||
stoweidlem23.3 | |
||
stoweidlem23.4 | |
||
stoweidlem23.5 | |
||
stoweidlem23.6 | |
||
stoweidlem23.7 | |
||
stoweidlem23.8 | |
||
stoweidlem23.9 | |
||
stoweidlem23.10 | |
||
Assertion | stoweidlem23 | |