mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: add competely normal (non-Hausdorff) property

Open StevenClontz opened this issue 1 year ago • 2 comments
trafficstars

This conribution adds a distinct notion of a (non-Hausdorff) completely normal space, and disintangles relevant results that do not require Hausdorff.

Open in Gitpod

StevenClontz avatar Apr 27 '24 03:04 StevenClontz

Oh, apparently mathlib doesn't know that totally disconnected spaces are T1. Will address that now.

StevenClontz avatar Apr 29 '24 02:04 StevenClontz

No clue why CI choked on 2ab0be8358a542996f1e5526a75721851622e0d7 and fb132c0d9d93f6c0377bc3311d9fc5b28d939ade but not f40a3033fd2af7c99ae3eccf2941eea145f9309c (and on files I didn't touch), but ah well. I believe this is now ready for review.

StevenClontz avatar Apr 29 '24 18:04 StevenClontz

bors merge

PatrickMassot avatar May 24 '24 16:05 PatrickMassot

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar May 24 '24 17:05 mathlib-bors[bot]