data.analysis

Stream: mathlib4

[Yury G. Kudryashov]

Are we going to port data.analysis or drop it?

[Patrick Massot]

I think people who feel this is important should feel free to port it. But I would be very sad to see you porting it.

[Yury G. Kudryashov]

If no one objects in a few days, I'll make a PR removing it from mathlib.

[Yuyang Zhao]

cc @Mario Carneiro

[Mario Carneiro]

Hm, I've thought this about several files that are being ported but I thought the idea was just to port these things anyway. In any case, I object to the removal.

[Mario Carneiro]

It's obviously not on the critical path, but I don't think it is an objectionable file. Would it make you feel better if it was in the computability folder?

[Mario Carneiro]

I have also heard this area called "descriptive set theory" although we don't have a folder for that

[Yury G. Kudryashov]

OK, not removing.