search

HoTT / book

A textbook on informal homotopy type theory
2.03k stars 361 forks source link

11.3.15 (extension of Lipschitz functions) incorrect #899

Open SkySkimmer opened 8 years ago

SkySkimmer commented 8 years ago

11.3.15 says Suppose f : Q → R is Lipschitz, then there exists f' : R -> R Lipschitz such that forall q, f'(rat q) = f q, but then in the proof it says for q : Q define f'(rat q) = rat (f q), ie using f : Q -> Q. This also breaks point (ii) (and (iii) since that's just symmetry of (ii)) as f'(lim x) ~Le f'(rat q) is f'(lim x) ~Le f q which cannot be proven by constructor of ~.

The explicit references to this lemma appear to be extending functions f : Q -> Q so the error seems to be in the statement of the lemma. I haven't checked in depth though.

andrejbauer commented 8 years ago

Upon a quick reading it looks like we could replace the offending definition with f'(rat q) = f q, could we not?

SkySkimmer commented 8 years ago

Then in (ii) the induction hypothesis is f'(x n) ~(L*e - L*n) f' (rat q) = f q and we need to prove f' (lim x) = lim (fun e => f' (x (e/L))) ~(L*e) ~ f q.

If we reorder things we can use 11.3.36 to do this.

andrejbauer commented 8 years ago

Ugh, we're committed to not reordering theorems. What to do?

mikeshulman commented 8 years ago

We could do some TeX hackery to reorder the theorems without renumbering them...

andrejbauer commented 8 years ago

I thought humor was not allowed on GitHub.

mikeshulman commented 8 years ago

If we only need to apply this lemma when f is given as Q -> Q, then we could just state and prove it in that case and make the more general version an exercise.

mikeshulman commented 7 years ago

Did we decide what to do about this?