Gabriel Ebner (Apr 12 2021 at 17:17):
Π i, E i and
pi_Lp p hp E are definitionally equal, but they have different norms (L^∞ and L^p, resp.). Is there a reason why
unique_diff_on (s : Π i, E i) and
unique_diff_on (s : pi_Lp p hp) should be definitionally equal?
(It is clear that they should be equivalent because everything is finite-dimensional. I'm asking because this broke while debugging #7124. Apparently you could use a proof of
unique_diff_on for L^∞ where a proof for L^2 was expected.)
Gabriel Ebner (Apr 12 2021 at 17:32):
On second thought, this is probably because
unique_diff_on never mentions the norm of the tuple, and the topologies are definitionally equal.
Sebastien Gouezel (Apr 12 2021 at 17:37):
I had never noticed that this definition only depends on the topology! We should probably refactor the typeclasses in
unique_diff_on to make this more obvious.
Yury G. Kudryashov (Apr 12 2021 at 20:01):
unique_diff_on.pi without realizing that Lean does some heavy identifying under the hood.
Last updated: May 09 2021 at 10:11 UTC