continuous is a structure

Stream: general

[Yaël Dillies]

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]

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]

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]

The relevant PR is #5035 btw.

[Reid Barton]

The main reason was the apply bug

[Reid Barton]

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