# Zulip Chat Archive

## Stream: maths

### Topic: Unique differentiability and definitional equality

#### Gabriel Ebner (Apr 12 2021 at 17:17):

The types `Π 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):

/me used `unique_diff_on.pi`

without realizing that Lean does some heavy identifying under the hood.

Last updated: May 09 2021 at 10:11 UTC