Commit 2023-08-15 15:52 ec5f4d95

View on Github →

feat: add Filter.Eventually.self_of_nhdsSet (#6497) Also add subset_of_mem_nhdsSet. From the Sphere Eversion Project.

Estimated changes

modified theorem nhdsSet_singleton
added theorem subset_of_mem_nhdsSet