Zulip Chat Archive

Stream: maths

Topic: linear_pmap

Nicolò Cavalleri (Dec 31 2022 at 18:29):

Out of curiosity, why was not linear_pmap defined on the whole domain similarly to what it is done for local_equiv? As in what are the advantages of the current design with respect to the design of local_equiv?

Yury G. Kudryashov (Dec 31 2022 at 22:49):

The main advantage is that = means what you expect.

Yury G. Kudryashov (Dec 31 2022 at 22:51):

I defined linear_pmap to prove Hahn-Banach Theorem in #2120.

Yury G. Kudryashov (Dec 31 2022 at 22:53):

Of course, this advantage comes with a disadvantage: you need to prove that the argument belongs to the domain.

Yury G. Kudryashov (Dec 31 2022 at 22:53):

If you think that the other approach works better, then feel free to try to make a refactor.

Last updated: Dec 20 2023 at 11:08 UTC