I would like to prove that the squaring function is continuous, by simply using mul_continuous, but it requires that one uses a pairing function, and for that function I don't now what is the idiomatic way to express that it is continuous.

I found a solution to this problem, but I don't find it satisfactory. I prove continuity of the function `(fun u => (u, u))`

using the following line:

`by apply: (cvg_pair (F := nbhs x)(G := nbhs x) (H := nbhs x)).`

Why do you find this proof unsatisfactory (apart from the fact that maybe such a lemma should exist in math-comp analysis)?

I don't find it satisfactory because `by apply: cvg_pair.`

fails and I have to make the terms `nbhs x`

appear at several places, even though the symbol `nbhs`

appears nowhere in the goal.

I hope that eventually people will be able to reason about continuity of a composed expression by just expressing that all functions in the expression are continuous, without having to mention filters.

Last updated: Jun 25 2024 at 17:02 UTC