Commit 2023-07-31 08:03 0938530e

View on Github →

feat(Topology/Order/NhdsSet): new file (#6161) Prove lemmas about neighborhoods of intervals. Some lemmas are TC-generalizations of lemmas from the Sphere Eversion Project.

Estimated changes

added theorem nhdsSet_insert
added theorem Icc_mem_nhdsSet_Icc
added theorem Icc_mem_nhdsSet_Ico
added theorem Icc_mem_nhdsSet_Ioc
added theorem Ici_mem_nhdsSet_Icc
added theorem Ici_mem_nhdsSet_Ici
added theorem Ici_mem_nhdsSet_Ico
added theorem Ici_mem_nhdsSet_Ioc
added theorem Ico_mem_nhdsSet_Icc
added theorem Ico_mem_nhdsSet_Ico
added theorem Ico_mem_nhdsSet_Ioc
added theorem Iic_mem_nhdsSet_Icc
added theorem Iic_mem_nhdsSet_Ico
added theorem Iic_mem_nhdsSet_Iic
added theorem Iic_mem_nhdsSet_Ioc
added theorem Iio_mem_nhdsSet_Icc
added theorem Iio_mem_nhdsSet_Ico
added theorem Iio_mem_nhdsSet_Ioc
added theorem Ioc_mem_nhdsSet_Icc
added theorem Ioc_mem_nhdsSet_Ico
added theorem Ioc_mem_nhdsSet_Ioc
added theorem Ioi_mem_nhdsSet_Icc
added theorem Ioi_mem_nhdsSet_Ico
added theorem Ioi_mem_nhdsSet_Ioc
added theorem Ioo_mem_nhdsSet_Icc
added theorem Ioo_mem_nhdsSet_Ico
added theorem Ioo_mem_nhdsSet_Ioc
added theorem nhdsSet_Icc
added theorem nhdsSet_Ici
added theorem nhdsSet_Ico
added theorem nhdsSet_Iic
added theorem nhdsSet_Iio
added theorem nhdsSet_Ioc
added theorem nhdsSet_Ioi
added theorem nhdsSet_Ioo