Commit 2024-02-15 19:01 ba213d0c

View on Github →

chore(Topology/OrderClosed): review API (#10570)

  • Generalize lemmas from OrderClosedTopology to ClosedIciTopology or ClosedIicTopology.
  • Deprecate isClosed_le'/isClosed_ge', use more readable isClosed_Iic/isClosed_Ici instead.

Estimated changes

modified theorem CovBy.nhdsWithin_Iio
modified theorem Icc_mem_nhdsWithin_Ici'
modified theorem Icc_mem_nhdsWithin_Ici
modified theorem Icc_mem_nhdsWithin_Iic'
modified theorem Icc_mem_nhdsWithin_Iic
modified theorem Icc_mem_nhdsWithin_Iio'
modified theorem Icc_mem_nhdsWithin_Iio
modified theorem Ici_mem_nhds
modified theorem Ico_mem_nhdsWithin_Ici'
modified theorem Ico_mem_nhdsWithin_Ici
modified theorem Ico_mem_nhdsWithin_Iic
modified theorem Ico_mem_nhdsWithin_Iio'
modified theorem Ico_mem_nhdsWithin_Iio
modified theorem Iic_mem_nhds
modified theorem Iio_mem_nhds
modified theorem Ioc_mem_nhdsWithin_Ici
modified theorem Ioc_mem_nhdsWithin_Iic'
modified theorem Ioc_mem_nhdsWithin_Iic
modified theorem Ioc_mem_nhdsWithin_Iio'
modified theorem Ioc_mem_nhdsWithin_Iio
modified theorem Ioi_mem_nhds
modified theorem Ioo_mem_nhdsWithin_Ici
modified theorem Ioo_mem_nhdsWithin_Iic
modified theorem Ioo_mem_nhdsWithin_Iio'
modified theorem Ioo_mem_nhdsWithin_Iio
modified theorem interior_Iio
modified theorem isOpen_Iio
modified theorem isOpen_Ioi