uniform_continuous.continuous

Stream: maths

[Patrick Massot]

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]

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]

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]

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

[Patrick Massot]

I can rewrite it using calc if you prefer

[Johannes Hölzl]

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]

Yes, this would be good!

[Patrick Massot]

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]

isn't this prod.map f f?

[Patrick Massot]

Indeed it is! But not by definition :sad:

[Patrick Massot]

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

[Johannes Hölzl]

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]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Alistair Tucker]

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]

@Johannes Hölzl see https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/calc.20iff/near/152245238