## Stream: maths

### Topic: uniform_continuous.continuous

#### Patrick Massot (Dec 20 2018 at 08:51):

Still trying to clean up topology stuff, I realized the proof that uniform continuous functions are continuous is pretty hard to read. @Johannes Hölzl how do you like the following proof:

lemma uniform_continuous.continuous [uniform_space β] {f : α → β}
(hf : uniform_continuous f) : continuous f :=
begin
rw continuous_iff_tendsto,
intro a,
have key : prod.mk (f a) ∘ f = (λ p : α×α, (f p.1, f p.2)) ∘ prod.mk a, by simp,
rw [tendsto_iff_comap, nhds_eq_comap_uniformity, nhds_eq_comap_uniformity, comap_comap_comp, key],
conv_rhs { rw ←comap_comap_comp },
apply comap_mono,
rw ←map_le_iff_le_comap,
exact hf
end


#### Johannes Hölzl (Dec 20 2018 at 08:53):

I don't like this at all. I'm okay with adding show or similar to the original proof. But replacing it with an arbitrary sequence of tactic calls doesn't make it more readable.

#### Patrick Massot (Dec 20 2018 at 08:53):

The main difference is I use nhds x = uniformity.comap (prod.mk x) instead of nhds x = uniformity.lift' (λs:set (α×α), {y | (x, y) ∈ s})

#### Patrick Massot (Dec 20 2018 at 08:54):

It's not all about using tactic instead of term mode, it's a math difference

#### Patrick Massot (Dec 20 2018 at 08:54):

I can rewrite it using calc if you prefer

#### Johannes Hölzl (Dec 20 2018 at 08:54):

This is indeed a good change. But it would be nice if the proof structure wouldn't be hidden behind the tactics.

#### Johannes Hölzl (Dec 20 2018 at 08:54):

Yes, this would be good!

#### Patrick Massot (Dec 20 2018 at 08:57):

The key annoyance (here and elsewhere in this corner of mathlib) is how Lean notation is far less legible that paper notation when it comes to pull-back and push-forward. And also we don't have notation for (λ p : α×α, (f p.1, f p.2)) (this one is probably solvable) Compare $U_\alpha \leq (f \times f)^*U_\beta$ and uniformity ≤ comap (λ p : α×α, (f p.1, f p.2)) uniformity

#### Mario Carneiro (Dec 20 2018 at 09:04):

isn't this prod.map f f?

#### Patrick Massot (Dec 20 2018 at 09:11):

Indeed it is! But not by definition :sad:

#### Patrick Massot (Dec 20 2018 at 09:11):

Johannes, do you think we should rewrite everything using this prod.map in the definition of uniform continuity?

#### Johannes Hölzl (Dec 20 2018 at 09:14):

ouch, I think prod.map should have a different def, (prod.map f g p).1 = f p.1 should be defeq

#### Johannes Hölzl (Dec 20 2018 at 09:15):

what about adding def prod.map₂ {α β} (f : α → β) (p : α × α) : β × β := (f p.1, f p.2)

#### Patrick Massot (Dec 20 2018 at 09:16):

This clever guy noticed how I love subscript 2 those days.

#### Mario Carneiro (Dec 20 2018 at 09:17):

I guess this can be map₂ f = map f f once the definition of map is fixed

#### Alistair Tucker (Dec 20 2018 at 09:39):

I used prod.map for a reformulation of cauchy_seq in the contraction mapping stuff, but it didn't seem well-supported with theorems. I also had to define a partial order on products.

#### Patrick Massot (Dec 20 2018 at 09:56):

Last updated: May 19 2021 at 03:22 UTC