Commit 2022-12-26 18:42 0de015fb

View on Github →

feat: port data.set.intervals.pi (#1223) I changed a single proof, Icc_diff_pi_univ_Ioo_subset because the simpa got lost somewhere along the way. It did produce an existential statement in the end but it was not the correct one it seems. Since the proof was easy enough to fix without simpa I just did that instead of figuring out what exactly is going wrong.

Estimated changes