Description: Lemma for bcth . The proof makes essential use of the Axiom of Dependent Choice axdc4uz , which in the form used here accepts a "selection" function F from each element of K to a nonempty subset of K , and the result function g maps g ( n + 1 ) to an element of F ( n , g ( n ) ) . The trick here is thus in the choice of F and K : we let K be the set of all tagged nonempty open sets (tagged here meaning that we have a point and an open set, in an ordered pair), and F ( k , <. x , z >. ) gives the set of all balls of size less than 1 / k , tagged by their centers, whose closures fit within the given open set z and miss M ( k ) .
Since M ( k ) is closed, z \ M ( k ) is open and also nonempty, since z is nonempty and M ( k ) has empty interior. Then there is some ball contained in it, and hence our function F is valid (it never maps to the empty set). Now starting at a point in the interior of U. ran M , DC gives us the function g all whose elements are constrained by F acting on the previous value. (This is all proven in this lemma.) Now g is a sequence of tagged open balls, forming an inclusion chain (see bcthlem2 ) and whose sizes tend to zero, since they are bounded above by 1 / k . Thus, the centers of these balls form a Cauchy sequence, and converge to a point x (see bcthlem4 ). Since the inclusion chain also ensures the closure of each ball is in the previous ball, the point x must be in all these balls (see bcthlem3 ) and hence misses each M ( k ) , contradicting the fact that x is in the interior of U. ran M (which was the starting point). (Contributed by Mario Carneiro, 6-Jan-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bcth.2 | |
|
bcthlem.4 | |
||
bcthlem.5 | |
||
bcthlem.6 | |
||
bcthlem5.7 | |
||
Assertion | bcthlem5 | |