## Stream: math-comp analysis

### Topic: Proving that (fun x => x ^ 2) is continuous

#### Yves Bertot (Jun 20 2021 at 20:23):

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.

#### Yves Bertot (Jun 21 2021 at 11:31):

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)).`

#### Michael Soegtrop (Jun 21 2021 at 12:06):

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

#### Yves Bertot (Jun 22 2021 at 14:09):

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: Feb 05 2023 at 08:28 UTC