Zulip Chat Archive

Stream: general

Topic: preorder on `local_equiv`/`local_homeomorph`


Yury G. Kudryashov (Jan 11 2022 at 18:04):

I want to add a preorder on local_equiv/local_homeomorph given by e ≤ e' = e.source ⊆ e'.source ∧ eq_on e e' e.source

Yury G. Kudryashov (Jan 11 2022 at 18:05):

The goal is to use it with Zorn lemma.

Yury G. Kudryashov (Jan 11 2022 at 18:07):

Should it be hidden in a locale?

Yury G. Kudryashov (Jan 11 2022 at 18:14):

It plays well, e.g., with the setoid instance on local_equiv.

Johan Commelin (Jan 11 2022 at 18:21):

I guess hiding it in a locale is the safe and conservative choice. But it looks to me like a very natural order, so I wouldn't think it's crazy to just make it the global default.


Last updated: Dec 20 2023 at 11:08 UTC