Zulip Chat Archive

Stream: general

Topic: continuous is a structure

Yaël Dillies (Feb 22 2022 at 19:45):

Can someone explain me the rationale behind making docs#continuous a one-field structure? especially why docs#is_open_map in contrast isn't. I'm now defining spectral maps and have to decide whether I will follow the same path.

Yaël Dillies (Feb 22 2022 at 19:46):

To be clear, spectral maps are continuous functions such that the preimage of a compact open set is compact (and open thanks to continuity). So I would say it makes sense to extend continuous, but I'd like your opinion.

Eric Rodriguez (Feb 22 2022 at 19:48):

the docs say "Registered as a structure to make sure it is not unfolded by Lean.", so I guess you want to figure out whether you want the definition to be easily unfoldable or not

Yaël Dillies (Feb 22 2022 at 19:48):

The relevant PR is #5035 btw.

Reid Barton (Feb 22 2022 at 19:48):

The main reason was the apply bug

Reid Barton (Feb 22 2022 at 19:50):

I would guess that is_open_map is of the same age as continuous but it's never really used, so there was no need to change it to a structure

Last updated: Aug 03 2023 at 10:10 UTC