§ Baire Category Theorem

§ Proof

def find_witness(Ds, p, eps):
 """returns a point 'w' such that `w ∈ Ds[i] ∀i` and that `|p - w| < eps`."""
 seq = []
 cur = D[0].get_close_pt(p, eps/3)) # cur is 'eps/3' close to p.
 d_scale = 1 # current distance is eps / 3^d
 yield cur
 # loop invariant: 'cur' is eps/3^d from p
 for k in range(1, infty):
   for i in range(0, k):
     d += 1
	 # 1. next is closer to to point than 'cur' is by (1/3)
     next = D[i].get_close_pt(cur, eps/3**d)
	 # 2. (cur, next) distance is a monotonic decreasing function of 'd',
	 #      so d(cur, next) > d(next, next')
	 # Proof:
	 # - dist(cur, next) <= dist(cur, p) + dist(p, next)
	 # - dist(cur, next) <= eps/3**(d) + eps/3**(d+1) <= 4 eps / 3**d
	 # - this dist(cur, next) is monotone decreasing in d, and thus
	 #   sequence is cauchy.
	 yield cur
	 cur = next

§ Corollary 1: Space cannot be union of non chonk

§ Proof of Corollary 1

§ Corollary 2: One of union is chonk

§ Proof of Corollary 2

§ Abstract Use: Swap Quantifiers

§ Application : Vanishing derivative pointwise implies fn is polynomial

§ Application : the reals are uncountable.

§ Application: Uniform boundedness