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: Oct 13 2024 at 01:02 UTC