Zulip Chat Archive

Stream: maths

Topic: uniform_continuous.continuous


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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})

view this post on Zulip Patrick Massot (Dec 20 2018 at 08:54):

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

view this post on Zulip Patrick Massot (Dec 20 2018 at 08:54):

I can rewrite it using calc if you prefer

view this post on Zulip 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.

view this post on Zulip Johannes Hölzl (Dec 20 2018 at 08:54):

Yes, this would be good!

view this post on Zulip 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α(f×f)UβU_\alpha \leq (f \times f)^*U_\beta and uniformity ≤ comap (λ p : α×α, (f p.1, f p.2)) uniformity

view this post on Zulip Mario Carneiro (Dec 20 2018 at 09:04):

isn't this prod.map f f?

view this post on Zulip Patrick Massot (Dec 20 2018 at 09:11):

Indeed it is! But not by definition :sad:

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johannes Hölzl (Dec 20 2018 at 09:15):

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

view this post on Zulip Patrick Massot (Dec 20 2018 at 09:16):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Dec 20 2018 at 09:56):

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


Last updated: May 19 2021 at 03:22 UTC