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
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