preorder on `local_equiv`/`local_homeomorph`

Stream: general

[Yury G. Kudryashov]

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]

The goal is to use it with Zorn lemma.

[Yury G. Kudryashov]

Should it be hidden in a locale?

[Yury G. Kudryashov]

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

[Johan Commelin]

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.