Deprecated. Use `map_continuous` instead.

Stream: mathlib4

[Jeremy Tan]

In Topology.ContinuousMap.Defs, Topology.ContinuousMap.Basic and Topology.Homotopy.Basic the following lemmas appear with a "deprecated" comment (and slightly different arguments) – not the tag we now have, for these comments were added before we introduced the tag.

/-- Deprecated. Use `map_continuous` instead. -/
protected theorem continuous (f : C(X, Y)) : Continuous f :=
  f.continuous_toFun

/-- Deprecated. Use `map_continuousAt` instead. -/
protected theorem continuousAt (f : C(α, β)) (x : α) : ContinuousAt f x :=
  map_continuousAt f x

/-- Deprecated. Use `map_continuous` instead. -/
protected theorem continuous (F : Homotopy f₀ f₁) : Continuous F :=
  F.continuous_toFun

But they're still being used. Can we just remove the "deprecated" comments?

[Kim Morrison]

Would it still be desirable to use the indicated replacements? If so, we should do that.

[Jeremy Tan]

/poll Would it still be desirable to use the indicated replacements?
Yes
No

[Jeremy Tan]

I think the answer is no; these lemmas allow dot notation for continuity too

[Jireh Loreaux]

That argument (dot notation) could be made for any lemma of the form Continuous f where f : SomeContinuousMapType. The whole point of these generic lemmas is that it reduces the number of lemmas needed (from quadratic in the height of the hierarchy to linear).

[Jeremy Tan]

You mean map_continuous(At)?

[Jireh Loreaux]

right, that's the generic lemma.

[Jireh Loreaux]

Personally, I wouldn't mind having the dot notation versions around so long as we don't have to write them explicitly in the code. That is, if these lemmas were autogenerated upon writing an instance of ContinuousMapClass, that would be fine with me, although I'm not sure if others share this sentiment.

[Jireh Loreaux]

I'm curious what @Anne Baanen thinks about this.