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: Aug 19 2022 at 21:02 UTC