felixpernegger

Adding cozero completemented (P61) to various spaces

3

I mainly used the argument from #1518 by @prabau. This completes S86, S84 and S24. The proposition from #1518 is probably not exhausted yet (i.e. can be applied to more...

Completing Line with two origins (S83)

1

@prabau I essentially just copied your proof on mathse and adjusted it for Strongly Paracompact. Not sure if theres a better way.

Completing relative prime topology (S52)

19

My archnemesis.

Lean formalisation.

1

I am sure this has been discussed to some degree before (something similar is even mentioned in the [original announcement](https://jdabbs.com/announcing-the-p-base/) of $\pi$-base 11 years ago), however I did not find...