Stream: math-comp analysis

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

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

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

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

view this post on Zulip 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: Aug 19 2022 at 21:02 UTC